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 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 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 is being_a_generation_from_squares
len f <> 0 by A1, Def14;
then (len f) + (len g) <> 0 by NAT_1:7;
then A3: len (f ^ g) <> 0 by FINSEQ_1:35;
for n being Nat st n <> 0 & n <= len (f ^ g) & not (f ^ g) /. n is being_an_amalgam_of_squares holds
ex i, j being Nat st
( ( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) or (f ^ g) /. n = ((f ^ g) /. i) + ((f ^ g) /. j) ) & i <> 0 & i < n & j <> 0 & j < n )

proof

let n be Nat; :: thesis: ( n <> 0 & n <= len (f ^ g) & not (f ^ g) /. n is being_an_amalgam_of_squares implies ex i, j being Nat st
( ( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) or (f ^ g) /. n = ((f ^ g) /. i) + ((f ^ g) /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) )
assume A4: ( n <> 0 & n <= len (f ^ g) ) ; :: thesis: ( (f ^ g) /. n is being_an_amalgam_of_squares or ex i, j being Nat st
( ( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) or (f ^ g) /. n = ((f ^ g) /. i) + ((f ^ g) /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) )
then A5: n <= (len f) + (len g) by FINSEQ_1:35;

A6: now

assume A7: n <= len f ; :: thesis: ( (f ^ g) /. n is being_an_amalgam_of_squares or ex i, j being Nat st
( ( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) or (f ^ g) /. n = ((f ^ g) /. i) + ((f ^ g) /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) )
then A8: (f ^ g) /. n = f /. n by A4, Lm4;
A9: ( f /. n is being_an_amalgam_of_squares & not (f ^ g) /. n is being_an_amalgam_of_squares implies ex i, j being Nat st
( ( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) or (f ^ g) /. n = ((f ^ g) /. i) + ((f ^ g) /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) ) by A4, A7, Lm4;

now

given k, l being Nat such that A10: ( ( f /. n = (f /. k) * (f /. l) or f /. n = (f /. k) + (f /. l) ) & k <> 0 & k < n & l <> 0 & l < n ) ; :: thesis: ( (f ^ g) /. n is being_an_amalgam_of_squares or ex i, j being Nat st
( ( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) or (f ^ g) /. n = ((f ^ g) /. i) + ((f ^ g) /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) )
A11: (f ^ g) /. k = f /. k by A7, A10, Lm4, XXREAL_0:2;
(f ^ g) /. l = f /. l by A7, A10, Lm4, XXREAL_0:2;
hence ( (f ^ g) /. n is being_an_amalgam_of_squares or ex i, j being Nat st
( ( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) or (f ^ g) /. n = ((f ^ g) /. i) + ((f ^ g) /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) ) by A8, A10, A11; :: thesis: verum

end;

hence ( (f ^ g) /. n is being_an_amalgam_of_squares or ex i, j being Nat st
( ( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) or (f ^ g) /. n = ((f ^ g) /. i) + ((f ^ g) /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) ) by A1, A4, A7, A9, Def14; :: thesis: verum

end;

now

assume A12: len f < n ; :: thesis: ( (f ^ g) /. n is being_an_amalgam_of_squares or ex i, j being Nat st
( ( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) or (f ^ g) /. n = ((f ^ g) /. i) + ((f ^ g) /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) )
then consider m being Nat such that
A13: n = (len f) + m by NAT_1:10;
A14: m <= len g by A5, A13, XREAL_1:8;
( m <> 0 & (len f) + m <= (len f) + (len g) ) by A4, A12, A13, FINSEQ_1:35;
then A15: ( m <> 0 & m <= len g ) by XREAL_1:8;
then A16: ( g /. m is being_an_amalgam_of_squares & not (f ^ g) /. n is being_an_amalgam_of_squares implies ex i, j being Nat st
( ( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) or (f ^ g) /. n = ((f ^ g) /. i) + ((f ^ g) /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) ) by A13, Lm5;

now

given k, l being Nat such that A17: ( ( g /. m = (g /. k) * (g /. l) or g /. m = (g /. k) + (g /. l) ) & k <> 0 & k < m & l <> 0 & l < m ) ; :: thesis: ( (f ^ g) /. n is being_an_amalgam_of_squares or ex i, j being Nat st
( ( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) or (f ^ g) /. n = ((f ^ g) /. i) + ((f ^ g) /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) )
A18: ( (f ^ g) /. n = ((f ^ g) /. ((len f) + k)) * ((f ^ g) /. ((len f) + l)) or (f ^ g) /. n = ((f ^ g) /. ((len f) + k)) + ((f ^ g) /. ((len f) + l)) )

proof

A19: now

assume g /. m = (g /. k) * (g /. l) ; :: thesis: ( (f ^ g) /. n = ((f ^ g) /. ((len f) + k)) * ((f ^ g) /. ((len f) + l)) or (f ^ g) /. n = ((f ^ g) /. ((len f) + k)) + ((f ^ g) /. ((len f) + l)) )
then (f ^ g) /. n = (g /. k) * (g /. l) by A13, A15, Lm5
.= ((f ^ g) /. ((len f) + k)) * (g /. l) by A14, A17, Lm5, XXREAL_0:2
.= ((f ^ g) /. ((len f) + k)) * ((f ^ g) /. ((len f) + l)) by A14, A17, Lm5, XXREAL_0:2 ;
hence ( (f ^ g) /. n = ((f ^ g) /. ((len f) + k)) * ((f ^ g) /. ((len f) + l)) or (f ^ g) /. n = ((f ^ g) /. ((len f) + k)) + ((f ^ g) /. ((len f) + l)) ) ; :: thesis: verum

end;

now

assume g /. m = (g /. k) + (g /. l) ; :: thesis: ( (f ^ g) /. n = ((f ^ g) /. ((len f) + k)) * ((f ^ g) /. ((len f) + l)) or (f ^ g) /. n = ((f ^ g) /. ((len f) + k)) + ((f ^ g) /. ((len f) + l)) )
then (f ^ g) /. n = (g /. k) + (g /. l) by A13, A15, Lm5
.= ((f ^ g) /. ((len f) + k)) + (g /. l) by A14, A17, Lm5, XXREAL_0:2
.= ((f ^ g) /. ((len f) + k)) + ((f ^ g) /. ((len f) + l)) by A14, A17, Lm5, XXREAL_0:2 ;
hence ( (f ^ g) /. n = ((f ^ g) /. ((len f) + k)) * ((f ^ g) /. ((len f) + l)) or (f ^ g) /. n = ((f ^ g) /. ((len f) + k)) + ((f ^ g) /. ((len f) + l)) ) ; :: thesis: verum

end;

hence ( (f ^ g) /. n = ((f ^ g) /. ((len f) + k)) * ((f ^ g) /. ((len f) + l)) or (f ^ g) /. n = ((f ^ g) /. ((len f) + k)) + ((f ^ g) /. ((len f) + l)) ) by A17, A19; :: thesis: verum

end;

A20: ( (len f) + k <> 0 & (len f) + l <> 0 ) by A17, NAT_1:7;
( (len f) + k < n & (len f) + l < n ) by A13, A17, XREAL_1:8;
hence ( (f ^ g) /. n is being_an_amalgam_of_squares or ex i, j being Nat st
( ( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) or (f ^ g) /. n = ((f ^ g) /. i) + ((f ^ g) /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) ) by A18, A20; :: thesis: verum

end;

hence ( (f ^ g) /. n is being_an_amalgam_of_squares or ex i, j being Nat st
( ( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) or (f ^ g) /. n = ((f ^ g) /. i) + ((f ^ g) /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) ) by A2, A15, A16, Def14; :: thesis: verum

end;

hence ( (f ^ g) /. n is being_an_amalgam_of_squares or ex i, j being Nat st
( ( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) or (f ^ g) /. n = ((f ^ g) /. i) + ((f ^ g) /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) ) by A6; :: thesis: verum

end;

hence f ^ g is being_a_generation_from_squares by A3, Def14; :: thesis: verum