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: len g <> 0 by A2;
len f <> 0 by A1;
then 1 <= len f by NAT_1:25;
then len f in dom f by FINSEQ_3:25;
then A4: ( (len f) + (len g) <= len (f ^ g) & (f ^ g) /. (len f) = f /. (len f) ) by Lm1, FINSEQ_1:22;
len f <= (len f) + (len g) by NAT_1:11;
then A5: len f <= len (f ^ g) by FINSEQ_1:22;
1 <= len g by A3, NAT_1:25;
then len g in dom g by FINSEQ_3:25;
then A6: (f ^ g) /. ((len f) + (len g)) = g /. (len g) by Lm1;
( f ^ g is being_a_generation_from_squares & len f <> 0 ) by A1, A2, Lm33;
hence (f ^ g) ^ <*((f /. (len f)) + (g /. (len g)))*> is being_a_generation_from_squares by A5, A4, A6, Lm61; :: thesis: verum