let R be non empty doubleLoopStr ; :: thesis: for f, g being FinSequence of R st f is being_a_generation_from_squares & g is being_a_generation_from_squares holds
(f ^ g) ^ <*((f /. (len f)) + (g /. (len g)))*> is being_a_generation_from_squares
let f, g be FinSequence of R; :: thesis: ( f is being_a_generation_from_squares & g is being_a_generation_from_squares implies (f ^ g) ^ <*((f /. (len f)) + (g /. (len g)))*> is being_a_generation_from_squares )
assume that
A1: f is being_a_generation_from_squares and
A2: g is being_a_generation_from_squares ; :: thesis: (f ^ g) ^ <*((f /. (len f)) + (g /. (len g)))*> is being_a_generation_from_squares
A3: f ^ g is being_a_generation_from_squares by A1, A2, Lm33;
A4: len f <> 0 by A1, Def14;
len f <= (len f) + (len g) by NAT_1:11;
then A5: ( len f <> 0 & len f <= len (f ^ g) ) by A1, Def14, FINSEQ_1:35;
A6: len g <> 0 by A2, Def14;
then A7: ( (len f) + (len g) <> 0 & (len f) + (len g) <= len (f ^ g) ) by FINSEQ_1:35, NAT_1:7;
( 1 <= len f & len f <= len f ) by A4, NAT_1:26;
then len f in dom f by FINSEQ_3:27;
then A8: (f ^ g) /. (len f) = f /. (len f) by Lm1;
( 1 <= len g & len g <= len g ) by A6, NAT_1:26;
then len g in dom g by FINSEQ_3:27;
then (f ^ g) /. ((len f) + (len g)) = g /. (len g) by Lm1;
hence (f ^ g) ^ <*((f /. (len f)) + (g /. (len g)))*> is being_a_generation_from_squares by A3, A5, A7, A8, Lm61; :: thesis: verum