7917

1 
(* Title: HOL/Real/HahnBanach/VectorSpace.thy


2 
ID: $Id$


3 
Author: Gertrud Bauer, TU Munich


4 
*)


5 


6 
header {* Vector spaces *};


7 


8 
theory VectorSpace = Bounds + Aux:;


9 


10 
subsection {* Signature *};


11 


12 
text {* For the definition of real vector spaces a type $\alpha$ is


13 
considered, on which the operations addition and real scalar


14 
multiplication are defined, and which has an zero element.*};


15 


16 
consts


17 
(***


18 
sum :: "['a, 'a] => 'a" (infixl "+" 65)


19 
***)


20 
prod :: "[real, 'a] => 'a" (infixr "<*>" 70)


21 
zero :: 'a ("<0>");


22 


23 
syntax (symbols)


24 
prod :: "[real, 'a] => 'a" (infixr "\<prod>" 70)


25 
zero :: 'a ("\<zero>");


26 


27 
text {* The unary and binary minus can be considered as


28 
abbreviations: *};


29 


30 
(***


31 
constdefs


32 
negate :: "'a => 'a" (" _" [100] 100)


33 
" x == ( 1r) <*> x"


34 
diff :: "'a => 'a => 'a" (infixl "" 68)


35 
"x  y == x +  y";


36 
***)


37 


38 
subsection {* Vector space laws *};


39 


40 
text {* A \emph{vector space} is a nonempty set $V$ of elements


41 
from $\alpha$ with the following vector space laws:


42 
The set $V$ is closed under addition and scalar multiplication,


43 
addition is associative and commutative. $\minus x$ is the inverse


44 
of $x$ w.~r.~t.~addition and $\zero$ is the neutral element of


45 
addition.


46 
Addition and multiplication are distributive.


47 
Scalar multiplication is associative and the real $1$ is the neutral


48 
element of scalar multiplication.


49 
*};


50 


51 
constdefs


52 
is_vectorspace :: "('a::{plus,minus}) set => bool"


53 
"is_vectorspace V == V ~= {}


54 
& (ALL x:V. ALL y:V. ALL z:V. ALL a b.


55 
x + y : V


56 
& a <*> x : V


57 
& x + y + z = x + (y + z)


58 
& x + y = y + x


59 
& x  x = <0>


60 
& <0> + x = x


61 
& a <*> (x + y) = a <*> x + a <*> y


62 
& (a + b) <*> x = a <*> x + b <*> x


63 
& (a * b) <*> x = a <*> b <*> x


64 
& 1r <*> x = x


65 
&  x = ( 1r) <*> x


66 
& x  y = x +  y)";


67 


68 
text_raw {* \medskip *};


69 
text {* The corresponding introduction rule is:*};


70 


71 
lemma vsI [intro]:


72 
"[ <0>:V;


73 
ALL x:V. ALL y:V. x + y : V;


74 
ALL x:V. ALL a. a <*> x : V;


75 
ALL x:V. ALL y:V. ALL z:V. x + y + z = x + (y + z);


76 
ALL x:V. ALL y:V. x + y = y + x;


77 
ALL x:V. x  x = <0>;


78 
ALL x:V. <0> + x = x;


79 
ALL x:V. ALL y:V. ALL a. a <*> (x + y) = a <*> x + a <*> y;


80 
ALL x:V. ALL a b. (a + b) <*> x = a <*> x + b <*> x;


81 
ALL x:V. ALL a b. (a * b) <*> x = a <*> b <*> x;


82 
ALL x:V. 1r <*> x = x;


83 
ALL x:V.  x = ( 1r) <*> x;


84 
ALL x:V. ALL y:V. x  y = x +  y] ==> is_vectorspace V";


85 
proof (unfold is_vectorspace_def, intro conjI ballI allI);


86 
fix x y z;


87 
assume "x:V" "y:V" "z:V"


88 
"ALL x:V. ALL y:V. ALL z:V. x + y + z = x + (y + z)";


89 
thus "x + y + z = x + (y + z)"; by (elim bspec[elimify]);


90 
qed force+;


91 


92 
text_raw {* \medskip *};


93 
text {* The corresponding destruction rules are: *};


94 


95 
lemma negate_eq1:


96 
"[ is_vectorspace V; x:V ] ==>  x = ( 1r) <*> x";


97 
by (unfold is_vectorspace_def) simp;


98 


99 
lemma diff_eq1:


100 
"[ is_vectorspace V; x:V; y:V ] ==> x  y = x +  y";


101 
by (unfold is_vectorspace_def) simp;


102 


103 
lemma negate_eq2:


104 
"[ is_vectorspace V; x:V ] ==> ( 1r) <*> x =  x";


105 
by (unfold is_vectorspace_def) simp;


106 


107 
lemma diff_eq2:


108 
"[ is_vectorspace V; x:V; y:V ] ==> x +  y = x  y";


109 
by (unfold is_vectorspace_def) simp;


110 


111 
lemma vs_not_empty [intro !!]: "is_vectorspace V ==> (V ~= {})";


112 
by (unfold is_vectorspace_def) simp;


113 


114 
lemma vs_add_closed [simp, intro!!]:


115 
"[ is_vectorspace V; x:V; y:V] ==> x + y : V";


116 
by (unfold is_vectorspace_def) simp;


117 


118 
lemma vs_mult_closed [simp, intro!!]:


119 
"[ is_vectorspace V; x:V ] ==> a <*> x : V";


120 
by (unfold is_vectorspace_def) simp;


121 


122 
lemma vs_diff_closed [simp, intro!!]:


123 
"[ is_vectorspace V; x:V; y:V] ==> x  y : V";


124 
by (simp add: diff_eq1 negate_eq1);


125 


126 
lemma vs_neg_closed [simp, intro!!]:


127 
"[ is_vectorspace V; x:V ] ==>  x : V";


128 
by (simp add: negate_eq1);


129 


130 
lemma vs_add_assoc [simp]:


131 
"[ is_vectorspace V; x:V; y:V; z:V]


132 
==> x + y + z = x + (y + z)";


133 
by (unfold is_vectorspace_def) fast;


134 


135 
lemma vs_add_commute [simp]:


136 
"[ is_vectorspace V; x:V; y:V ] ==> y + x = x + y";


137 
by (unfold is_vectorspace_def) simp;


138 


139 
lemma vs_add_left_commute [simp]:


140 
"[ is_vectorspace V; x:V; y:V; z:V ]


141 
==> x + (y + z) = y + (x + z)";


142 
proof ;


143 
assume "is_vectorspace V" "x:V" "y:V" "z:V";


144 
hence "x + (y + z) = (x + y) + z";


145 
by (simp only: vs_add_assoc);


146 
also; have "... = (y + x) + z"; by (simp! only: vs_add_commute);


147 
also; have "... = y + (x + z)"; by (simp! only: vs_add_assoc);


148 
finally; show ?thesis; .;


149 
qed;


150 


151 
theorems vs_add_ac = vs_add_assoc vs_add_commute vs_add_left_commute;


152 


153 
lemma vs_diff_self [simp]:


154 
"[ is_vectorspace V; x:V ] ==> x  x = <0>";


155 
by (unfold is_vectorspace_def) simp;


156 


157 
text {* The existence of the zero element a vector space


158 
follows from the nonemptyness of the vector space. *};


159 


160 
lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> <0>:V";


161 
proof ;


162 
assume "is_vectorspace V";


163 
have "V ~= {}"; ..;


164 
hence "EX x. x:V"; by force;


165 
thus ?thesis;


166 
proof;


167 
fix x; assume "x:V";


168 
have "<0> = x  x"; by (simp!);


169 
also; have "... : V"; by (simp! only: vs_diff_closed);


170 
finally; show ?thesis; .;


171 
qed;


172 
qed;


173 


174 
lemma vs_add_zero_left [simp]:


175 
"[ is_vectorspace V; x:V ] ==> <0> + x = x";


176 
by (unfold is_vectorspace_def) simp;


177 


178 
lemma vs_add_zero_right [simp]:


179 
"[ is_vectorspace V; x:V ] ==> x + <0> = x";


180 
proof ;


181 
assume "is_vectorspace V" "x:V";


182 
hence "x + <0> = <0> + x"; by simp;


183 
also; have "... = x"; by (simp!);


184 
finally; show ?thesis; .;


185 
qed;


186 


187 
lemma vs_add_mult_distrib1:


188 
"[ is_vectorspace V; x:V; y:V ]


189 
==> a <*> (x + y) = a <*> x + a <*> y";


190 
by (unfold is_vectorspace_def) simp;


191 


192 
lemma vs_add_mult_distrib2:


193 
"[ is_vectorspace V; x:V ]


194 
==> (a + b) <*> x = a <*> x + b <*> x";


195 
by (unfold is_vectorspace_def) simp;


196 


197 
lemma vs_mult_assoc:


198 
"[ is_vectorspace V; x:V ] ==> (a * b) <*> x = a <*> (b <*> x)";


199 
by (unfold is_vectorspace_def) simp;


200 


201 
lemma vs_mult_assoc2 [simp]:


202 
"[ is_vectorspace V; x:V ] ==> a <*> b <*> x = (a * b) <*> x";


203 
by (simp only: vs_mult_assoc);


204 


205 
lemma vs_mult_1 [simp]:


206 
"[ is_vectorspace V; x:V ] ==> 1r <*> x = x";


207 
by (unfold is_vectorspace_def) simp;


208 


209 
lemma vs_diff_mult_distrib1:


210 
"[ is_vectorspace V; x:V; y:V ]


211 
==> a <*> (x  y) = a <*> x  a <*> y";


212 
by (simp add: diff_eq1 negate_eq1 vs_add_mult_distrib1);


213 


214 
lemma vs_diff_mult_distrib2:


215 
"[ is_vectorspace V; x:V ]


216 
==> (a  b) <*> x = a <*> x  (b <*> x)";


217 
proof ;


218 
assume "is_vectorspace V" "x:V";


219 
have " (a  b) <*> x = (a +  b ) <*> x";


220 
by (unfold real_diff_def, simp);


221 
also; have "... = a <*> x + ( b) <*> x";


222 
by (rule vs_add_mult_distrib2);


223 
also; have "... = a <*> x +  (b <*> x)";


224 
by (simp! add: negate_eq1);


225 
also; have "... = a <*> x  (b <*> x)";


226 
by (simp! add: diff_eq1);


227 
finally; show ?thesis; .;


228 
qed;


229 


230 
(*text_raw {* \paragraph {Further derived laws:} *};*)


231 
text_raw {* \medskip *};


232 
text{* Further derived laws: *};


233 


234 
lemma vs_mult_zero_left [simp]:


235 
"[ is_vectorspace V; x:V] ==> 0r <*> x = <0>";


236 
proof ;


237 
assume "is_vectorspace V" "x:V";


238 
have "0r <*> x = (1r  1r) <*> x"; by (simp only: real_diff_self);


239 
also; have "... = (1r +  1r) <*> x"; by simp;


240 
also; have "... = 1r <*> x + ( 1r) <*> x";


241 
by (rule vs_add_mult_distrib2);


242 
also; have "... = x + ( 1r) <*> x"; by (simp!);


243 
also; have "... = x +  x"; by (simp! add: negate_eq2);;


244 
also; have "... = x  x"; by (simp! add: diff_eq2);


245 
also; have "... = <0>"; by (simp!);


246 
finally; show ?thesis; .;


247 
qed;


248 


249 
lemma vs_mult_zero_right [simp]:


250 
"[ is_vectorspace (V:: 'a::{plus, minus} set) ]


251 
==> a <*> <0> = (<0>::'a)";


252 
proof ;


253 
assume "is_vectorspace V";


254 
have "a <*> <0> = a <*> (<0>  (<0>::'a))"; by (simp!);


255 
also; have "... = a <*> <0>  a <*> <0>";


256 
by (rule vs_diff_mult_distrib1) (simp!)+;


257 
also; have "... = <0>"; by (simp!);


258 
finally; show ?thesis; .;


259 
qed;


260 


261 
lemma vs_minus_mult_cancel [simp]:


262 
"[ is_vectorspace V; x:V ] ==> ( a) <*>  x = a <*> x";


263 
by (simp add: negate_eq1);


264 


265 
lemma vs_add_minus_left_eq_diff:


266 
"[ is_vectorspace V; x:V; y:V ] ==>  x + y = y  x";


267 
proof ;


268 
assume "is_vectorspace V" "x:V" "y:V";


269 
have " x + y = y +  x";


270 
by (simp! add: vs_add_commute [RS sym, of V " x"]);


271 
also; have "... = y  x"; by (simp! add: diff_eq1);


272 
finally; show ?thesis; .;


273 
qed;


274 


275 
lemma vs_add_minus [simp]:


276 
"[ is_vectorspace V; x:V ] ==> x +  x = <0>";


277 
by (simp! add: diff_eq2);


278 


279 
lemma vs_add_minus_left [simp]:


280 
"[ is_vectorspace V; x:V ] ==>  x + x = <0>";


281 
by (simp! add: diff_eq2);


282 


283 
lemma vs_minus_minus [simp]:


284 
"[ is_vectorspace V; x:V ] ==>  ( x) = x";


285 
by (simp add: negate_eq1);


286 


287 
lemma vs_minus_zero [simp]:


288 
"is_vectorspace (V::'a::{minus, plus} set) ==>  (<0>::'a) = <0>";


289 
by (simp add: negate_eq1);


290 


291 
lemma vs_minus_zero_iff [simp]:


292 
"[ is_vectorspace V; x:V ] ==> ( x = <0>) = (x = <0>)"


293 
(concl is "?L = ?R");


294 
proof ;


295 
assume "is_vectorspace V" "x:V";


296 
show "?L = ?R";


297 
proof;


298 
have "x =  ( x)"; by (rule vs_minus_minus [RS sym]);


299 
also; assume ?L;


300 
also; have " ... = <0>"; by (rule vs_minus_zero);


301 
finally; show ?R; .;


302 
qed (simp!);


303 
qed;


304 


305 
lemma vs_add_minus_cancel [simp]:


306 
"[ is_vectorspace V; x:V; y:V ] ==> x + ( x + y) = y";


307 
by (simp add: vs_add_assoc [RS sym] del: vs_add_commute);


308 


309 
lemma vs_minus_add_cancel [simp]:


310 
"[ is_vectorspace V; x:V; y:V ] ==>  x + (x + y) = y";


311 
by (simp add: vs_add_assoc [RS sym] del: vs_add_commute);


312 


313 
lemma vs_minus_add_distrib [simp]:


314 
"[ is_vectorspace V; x:V; y:V ]


315 
==>  (x + y) =  x +  y";


316 
by (simp add: negate_eq1 vs_add_mult_distrib1);


317 


318 
lemma vs_diff_zero [simp]:


319 
"[ is_vectorspace V; x:V ] ==> x  <0> = x";


320 
by (simp add: diff_eq1);


321 


322 
lemma vs_diff_zero_right [simp]:


323 
"[ is_vectorspace V; x:V ] ==> <0>  x =  x";


324 
by (simp add:diff_eq1);


325 


326 
lemma vs_add_left_cancel:


327 
"[ is_vectorspace V; x:V; y:V; z:V]


328 
==> (x + y = x + z) = (y = z)"


329 
(concl is "?L = ?R");


330 
proof;


331 
assume "is_vectorspace V" "x:V" "y:V" "z:V";


332 
have "y = <0> + y"; by (simp!);


333 
also; have "... =  x + x + y"; by (simp!);


334 
also; have "... =  x + (x + y)";


335 
by (simp! only: vs_add_assoc vs_neg_closed);


336 
also; assume ?L;


337 
also; have " x + ... =  x + x + z";


338 
by (rule vs_add_assoc [RS sym]) (simp!)+;


339 
also; have "... = z"; by (simp!);


340 
finally; show ?R;.;


341 
qed force;


342 


343 
lemma vs_add_right_cancel:


344 
"[ is_vectorspace V; x:V; y:V; z:V ]


345 
==> (y + x = z + x) = (y = z)";


346 
by (simp only: vs_add_commute vs_add_left_cancel);


347 


348 
lemma vs_add_assoc_cong:


349 
"[ is_vectorspace V; x:V; y:V; x':V; y':V; z:V ]


350 
==> x + y = x' + y' ==> x + (y + z) = x' + (y' + z)";


351 
by (simp only: vs_add_assoc [RS sym]);


352 


353 
lemma vs_mult_left_commute:


354 
"[ is_vectorspace V; x:V; y:V; z:V ]


355 
==> x <*> y <*> z = y <*> x <*> z";


356 
by (simp add: real_mult_commute);


357 


358 
lemma vs_mult_zero_uniq :


359 
"[ is_vectorspace V; x:V; a <*> x = <0>; x ~= <0> ] ==> a = 0r";


360 
proof (rule classical);


361 
assume "is_vectorspace V" "x:V" "a <*> x = <0>" "x ~= <0>";


362 
assume "a ~= 0r";


363 
have "x = (rinv a * a) <*> x"; by (simp!);


364 
also; have "... = rinv a <*> (a <*> x)"; by (rule vs_mult_assoc);


365 
also; have "... = rinv a <*> <0>"; by (simp!);


366 
also; have "... = <0>"; by (simp!);


367 
finally; have "x = <0>"; .;


368 
thus "a = 0r"; by contradiction;


369 
qed;


370 


371 
lemma vs_mult_left_cancel:


372 
"[ is_vectorspace V; x:V; y:V; a ~= 0r ] ==>


373 
(a <*> x = a <*> y) = (x = y)"


374 
(concl is "?L = ?R");


375 
proof;


376 
assume "is_vectorspace V" "x:V" "y:V" "a ~= 0r";


377 
have "x = 1r <*> x"; by (simp!);


378 
also; have "... = (rinv a * a) <*> x"; by (simp!);


379 
also; have "... = rinv a <*> (a <*> x)";


380 
by (simp! only: vs_mult_assoc);


381 
also; assume ?L;


382 
also; have "rinv a <*> ... = y"; by (simp!);


383 
finally; show ?R;.;


384 
qed simp;


385 


386 
lemma vs_mult_right_cancel: (*** forward ***)


387 
"[ is_vectorspace V; x:V; x ~= <0> ]


388 
==> (a <*> x = b <*> x) = (a = b)" (concl is "?L = ?R");


389 
proof;


390 
assume "is_vectorspace V" "x:V" "x ~= <0>";


391 
have "(a  b) <*> x = a <*> x  b <*> x";


392 
by (simp! add: vs_diff_mult_distrib2);


393 
also; assume ?L; hence "a <*> x  b <*> x = <0>"; by (simp!);


394 
finally; have "(a  b) <*> x = <0>"; .;


395 
hence "a  b = 0r"; by (simp! add: vs_mult_zero_uniq);


396 
thus "a = b"; by (rule real_add_minus_eq);


397 
qed simp; (***


398 


399 
backward :


400 
lemma vs_mult_right_cancel:


401 
"[ is_vectorspace V; x:V; x ~= <0> ] ==>


402 
(a <*> x = b <*> x) = (a = b)"


403 
(concl is "?L = ?R");


404 
proof;


405 
assume "is_vectorspace V" "x:V" "x ~= <0>";


406 
assume l: ?L;


407 
show "a = b";


408 
proof (rule real_add_minus_eq);


409 
show "a  b = 0r";


410 
proof (rule vs_mult_zero_uniq);


411 
have "(a  b) <*> x = a <*> x  b <*> x";


412 
by (simp! add: vs_diff_mult_distrib2);


413 
also; from l; have "a <*> x  b <*> x = <0>"; by (simp!);


414 
finally; show "(a  b) <*> x = <0>"; .;


415 
qed;


416 
qed;


417 
next;


418 
assume ?R;


419 
thus ?L; by simp;


420 
qed;


421 
**)


422 


423 
lemma vs_eq_diff_eq:


424 
"[ is_vectorspace V; x:V; y:V; z:V ] ==>


425 
(x = z  y) = (x + y = z)"


426 
(concl is "?L = ?R" );


427 
proof ;


428 
assume vs: "is_vectorspace V" "x:V" "y:V" "z:V";


429 
show "?L = ?R";


430 
proof;


431 
assume ?L;


432 
hence "x + y = z  y + y"; by simp;


433 
also; have "... = z +  y + y"; by (simp! add: diff_eq1);


434 
also; have "... = z + ( y + y)";


435 
by (rule vs_add_assoc) (simp!)+;


436 
also; from vs; have "... = z + <0>";


437 
by (simp only: vs_add_minus_left);


438 
also; from vs; have "... = z"; by (simp only: vs_add_zero_right);


439 
finally; show ?R;.;


440 
next;


441 
assume ?R;


442 
hence "z  y = (x + y)  y"; by simp;


443 
also; from vs; have "... = x + y +  y";


444 
by (simp add: diff_eq1);


445 
also; have "... = x + (y +  y)";


446 
by (rule vs_add_assoc) (simp!)+;


447 
also; have "... = x"; by (simp!);


448 
finally; show ?L; by (rule sym);


449 
qed;


450 
qed;


451 


452 
lemma vs_add_minus_eq_minus:


453 
"[ is_vectorspace V; x:V; y:V; x + y = <0>] ==> x =  y";


454 
proof ;


455 
assume "is_vectorspace V" "x:V" "y:V";


456 
have "x = ( y + y) + x"; by (simp!);


457 
also; have "... =  y + (x + y)"; by (simp!);


458 
also; assume "x + y = <0>";


459 
also; have " y + <0> =  y"; by (simp!);


460 
finally; show "x =  y"; .;


461 
qed;


462 


463 
lemma vs_add_minus_eq:


464 
"[ is_vectorspace V; x:V; y:V; x  y = <0> ] ==> x = y";


465 
proof ;


466 
assume "is_vectorspace V" "x:V" "y:V" "x  y = <0>";


467 
assume "x  y = <0>";


468 
hence e: "x +  y = <0>"; by (simp! add: diff_eq1);


469 
with _ _ _; have "x =  ( y)";


470 
by (rule vs_add_minus_eq_minus) (simp!)+;


471 
thus "x = y"; by (simp!);


472 
qed;


473 


474 
lemma vs_add_diff_swap:


475 
"[ is_vectorspace V; a:V; b:V; c:V; d:V; a + b = c + d]


476 
==> a  c = d  b";


477 
proof ;


478 
assume vs: "is_vectorspace V" "a:V" "b:V" "c:V" "d:V"


479 
and eq: "a + b = c + d";


480 
have " c + (a + b) =  c + (c + d)";


481 
by (simp! add: vs_add_left_cancel);


482 
also; have "... = d"; by (rule vs_minus_add_cancel);


483 
finally; have eq: " c + (a + b) = d"; .;


484 
from vs; have "a  c = ( c + (a + b)) +  b";


485 
by (simp add: vs_add_ac diff_eq1);


486 
also; from eq; have "... = d +  b";


487 
by (simp! add: vs_add_right_cancel);


488 
also; have "... = d  b"; by (simp! add : diff_eq2);


489 
finally; show "a  c = d  b"; .;


490 
qed;


491 


492 
lemma vs_add_cancel_21:


493 
"[ is_vectorspace V; x:V; y:V; z:V; u:V]


494 
==> (x + (y + z) = y + u) = ((x + z) = u)"


495 
(concl is "?L = ?R" );


496 
proof ;


497 
assume "is_vectorspace V" "x:V" "y:V""z:V" "u:V";


498 
show "?L = ?R";


499 
proof;


500 
have "x + z =  y + y + (x + z)"; by (simp!);


501 
also; have "... =  y + (y + (x + z))";


502 
by (rule vs_add_assoc) (simp!)+;


503 
also; have "y + (x + z) = x + (y + z)"; by (simp!);


504 
also; assume ?L;


505 
also; have " y + (y + u) = u"; by (simp!);


506 
finally; show ?R; .;


507 
qed (simp! only: vs_add_left_commute [of V x]);


508 
qed;


509 


510 
lemma vs_add_cancel_end:


511 
"[ is_vectorspace V; x:V; y:V; z:V ]


512 
==> (x + (y + z) = y) = (x =  z)"


513 
(concl is "?L = ?R" );


514 
proof ;


515 
assume "is_vectorspace V" "x:V" "y:V" "z:V";


516 
show "?L = ?R";


517 
proof;


518 
assume l: ?L;


519 
have "x + z = <0>";


520 
proof (rule vs_add_left_cancel [RS iffD1]);


521 
have "y + (x + z) = x + (y + z)"; by (simp!);


522 
also; note l;


523 
also; have "y = y + <0>"; by (simp!);


524 
finally; show "y + (x + z) = y + <0>"; .;


525 
qed (simp!)+;


526 
thus "x =  z"; by (simp! add: vs_add_minus_eq_minus);


527 
next;


528 
assume r: ?R;


529 
hence "x + (y + z) =  z + (y + z)"; by simp;


530 
also; have "... = y + ( z + z)";


531 
by (simp! only: vs_add_left_commute);


532 
also; have "... = y"; by (simp!);


533 
finally; show ?L; .;


534 
qed;


535 
qed;


536 


537 
end; 