let i, j be Nat; :: thesis: for R being non empty doubleLoopStr
for f being FinSequence of R st f is being_a_generation_from_squares & i <> 0 & i <= len f & j <> 0 & j <= len f holds
f ^ <*((f /. i) + (f /. j))*> is being_a_generation_from_squares
let R be non empty doubleLoopStr ; :: thesis: for f being FinSequence of R st f is being_a_generation_from_squares & i <> 0 & i <= len f & j <> 0 & j <= len f holds
f ^ <*((f /. i) + (f /. j))*> is being_a_generation_from_squares
let f be FinSequence of R; :: thesis: ( f is being_a_generation_from_squares & i <> 0 & i <= len f & j <> 0 & j <= len f implies f ^ <*((f /. i) + (f /. j))*> is being_a_generation_from_squares )
assume that
A1: f is being_a_generation_from_squares and
A2: i <> 0 and
A3: i <= len f and
A4: j <> 0 and
A5: j <= len f ; :: thesis: f ^ <*((f /. i) + (f /. j))*> is being_a_generation_from_squares
set g = f ^ <*((f /. i) + (f /. j))*>;
A6: len (f ^ <*((f /. i) + (f /. j))*>) = (len f) + (len <*((f /. i) + (f /. j))*>) by FINSEQ_1:22
.= (len f) + 1 by Lm2 ;
A7: for n being Nat st n <> 0 & n <= len (f ^ <*((f /. i) + (f /. j))*>) & not (f ^ <*((f /. i) + (f /. j))*>) /. n is being_an_amalgam_of_squares holds
ex i, j being Nat st
( ( (f ^ <*((f /. i) + (f /. j))*>) /. n = ((f ^ <*((f /. i) + (f /. j))*>) /. i) * ((f ^ <*((f /. i) + (f /. j))*>) /. j) or (f ^ <*((f /. i) + (f /. j))*>) /. n = ((f ^ <*((f /. i) + (f /. j))*>) /. i) + ((f ^ <*((f /. i) + (f /. j))*>) /. j) ) & i <> 0 & i < n & j <> 0 & j < n )

proof

let n be Nat; :: thesis: ( n <> 0 & n <= len (f ^ <*((f /. i) + (f /. j))*>) & not (f ^ <*((f /. i) + (f /. j))*>) /. n is being_an_amalgam_of_squares implies ex i, j being Nat st
( ( (f ^ <*((f /. i) + (f /. j))*>) /. n = ((f ^ <*((f /. i) + (f /. j))*>) /. i) * ((f ^ <*((f /. i) + (f /. j))*>) /. j) or (f ^ <*((f /. i) + (f /. j))*>) /. n = ((f ^ <*((f /. i) + (f /. j))*>) /. i) + ((f ^ <*((f /. i) + (f /. j))*>) /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) )
assume that
A8: n <> 0 and
A9: n <= len (f ^ <*((f /. i) + (f /. j))*>) ; :: thesis: ( (f ^ <*((f /. i) + (f /. j))*>) /. n is being_an_amalgam_of_squares or ex i, j being Nat st
( ( (f ^ <*((f /. i) + (f /. j))*>) /. n = ((f ^ <*((f /. i) + (f /. j))*>) /. i) * ((f ^ <*((f /. i) + (f /. j))*>) /. j) or (f ^ <*((f /. i) + (f /. j))*>) /. n = ((f ^ <*((f /. i) + (f /. j))*>) /. i) + ((f ^ <*((f /. i) + (f /. j))*>) /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) )

A10: now :: thesis: ( n < len (f ^ <*((f /. i) + (f /. j))*>) & not (f ^ <*((f /. i) + (f /. j))*>) /. n is being_an_amalgam_of_squares implies ex i, j being Nat st
( ( (f ^ <*((f /. i) + (f /. j))*>) /. n = ((f ^ <*((f /. i) + (f /. j))*>) /. i) * ((f ^ <*((f /. i) + (f /. j))*>) /. j) or (f ^ <*((f /. i) + (f /. j))*>) /. n = ((f ^ <*((f /. i) + (f /. j))*>) /. i) + ((f ^ <*((f /. i) + (f /. j))*>) /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) )

assume n < len (f ^ <*((f /. i) + (f /. j))*>) ; :: thesis: ( (f ^ <*((f /. i) + (f /. j))*>) /. n is being_an_amalgam_of_squares or ex i, j being Nat st
( ( (f ^ <*((f /. i) + (f /. j))*>) /. n = ((f ^ <*((f /. i) + (f /. j))*>) /. i) * ((f ^ <*((f /. i) + (f /. j))*>) /. j) or (f ^ <*((f /. i) + (f /. j))*>) /. n = ((f ^ <*((f /. i) + (f /. j))*>) /. i) + ((f ^ <*((f /. i) + (f /. j))*>) /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) )
then A11: n <= len f by A6, NAT_1:13;
then A12: (f ^ <*((f /. i) + (f /. j))*>) /. n = f /. n by A8, Lm4;

A13: now :: thesis: ( ex k, m being Nat st
( ( f /. n = (f /. k) * (f /. m) or f /. n = (f /. k) + (f /. m) ) & k <> 0 & k < n & m <> 0 & m < n ) & not (f ^ <*((f /. i) + (f /. j))*>) /. n is being_an_amalgam_of_squares implies ex i, j being Nat st
( ( (f ^ <*((f /. i) + (f /. j))*>) /. n = ((f ^ <*((f /. i) + (f /. j))*>) /. i) * ((f ^ <*((f /. i) + (f /. j))*>) /. j) or (f ^ <*((f /. i) + (f /. j))*>) /. n = ((f ^ <*((f /. i) + (f /. j))*>) /. i) + ((f ^ <*((f /. i) + (f /. j))*>) /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) )

given k, m being Nat such that A14: ( f /. n = (f /. k) * (f /. m) or f /. n = (f /. k) + (f /. m) ) and
A15: ( k <> 0 & k < n & m <> 0 & m < n ) ; :: thesis: ( (f ^ <*((f /. i) + (f /. j))*>) /. n is being_an_amalgam_of_squares or ex i, j being Nat st
( ( (f ^ <*((f /. i) + (f /. j))*>) /. n = ((f ^ <*((f /. i) + (f /. j))*>) /. i) * ((f ^ <*((f /. i) + (f /. j))*>) /. j) or (f ^ <*((f /. i) + (f /. j))*>) /. n = ((f ^ <*((f /. i) + (f /. j))*>) /. i) + ((f ^ <*((f /. i) + (f /. j))*>) /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) )
( f /. k = (f ^ <*((f /. i) + (f /. j))*>) /. k & f /. m = (f ^ <*((f /. i) + (f /. j))*>) /. m ) by A11, A15, Lm4, XXREAL_0:2;
hence ( (f ^ <*((f /. i) + (f /. j))*>) /. n is being_an_amalgam_of_squares or ex i, j being Nat st
( ( (f ^ <*((f /. i) + (f /. j))*>) /. n = ((f ^ <*((f /. i) + (f /. j))*>) /. i) * ((f ^ <*((f /. i) + (f /. j))*>) /. j) or (f ^ <*((f /. i) + (f /. j))*>) /. n = ((f ^ <*((f /. i) + (f /. j))*>) /. i) + ((f ^ <*((f /. i) + (f /. j))*>) /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) ) by A12, A14, A15; :: thesis: verum

end;

( f /. n is being_an_amalgam_of_squares & not (f ^ <*((f /. i) + (f /. j))*>) /. n is being_an_amalgam_of_squares implies ex i, j being Nat st
( ( (f ^ <*((f /. i) + (f /. j))*>) /. n = ((f ^ <*((f /. i) + (f /. j))*>) /. i) * ((f ^ <*((f /. i) + (f /. j))*>) /. j) or (f ^ <*((f /. i) + (f /. j))*>) /. n = ((f ^ <*((f /. i) + (f /. j))*>) /. i) + ((f ^ <*((f /. i) + (f /. j))*>) /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) ) by A8, A11, Lm4;
hence ( (f ^ <*((f /. i) + (f /. j))*>) /. n is being_an_amalgam_of_squares or ex i, j being Nat st
( ( (f ^ <*((f /. i) + (f /. j))*>) /. n = ((f ^ <*((f /. i) + (f /. j))*>) /. i) * ((f ^ <*((f /. i) + (f /. j))*>) /. j) or (f ^ <*((f /. i) + (f /. j))*>) /. n = ((f ^ <*((f /. i) + (f /. j))*>) /. i) + ((f ^ <*((f /. i) + (f /. j))*>) /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) ) by A1, A8, A11, A13; :: thesis: verum

end;

now :: thesis: ( n = len (f ^ <*((f /. i) + (f /. j))*>) & not (f ^ <*((f /. i) + (f /. j))*>) /. n is being_an_amalgam_of_squares implies ex i, j being Nat st
( ( (f ^ <*((f /. i) + (f /. j))*>) /. n = ((f ^ <*((f /. i) + (f /. j))*>) /. i) * ((f ^ <*((f /. i) + (f /. j))*>) /. j) or (f ^ <*((f /. i) + (f /. j))*>) /. n = ((f ^ <*((f /. i) + (f /. j))*>) /. i) + ((f ^ <*((f /. i) + (f /. j))*>) /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) )

assume A16: n = len (f ^ <*((f /. i) + (f /. j))*>) ; :: thesis: ( (f ^ <*((f /. i) + (f /. j))*>) /. n is being_an_amalgam_of_squares or ex i, j being Nat st
( ( (f ^ <*((f /. i) + (f /. j))*>) /. n = ((f ^ <*((f /. i) + (f /. j))*>) /. i) * ((f ^ <*((f /. i) + (f /. j))*>) /. j) or (f ^ <*((f /. i) + (f /. j))*>) /. n = ((f ^ <*((f /. i) + (f /. j))*>) /. i) + ((f ^ <*((f /. i) + (f /. j))*>) /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) )
then A17: ( i < n & j < n ) by A3, A5, A6, NAT_1:13;
(f ^ <*((f /. i) + (f /. j))*>) /. n = (f /. i) + (f /. j) by A6, A16, Lm3
.= ((f ^ <*((f /. i) + (f /. j))*>) /. i) + (f /. j) by A2, A3, Lm4
.= ((f ^ <*((f /. i) + (f /. j))*>) /. i) + ((f ^ <*((f /. i) + (f /. j))*>) /. j) by A4, A5, Lm4 ;
hence ( (f ^ <*((f /. i) + (f /. j))*>) /. n is being_an_amalgam_of_squares or ex i, j being Nat st
( ( (f ^ <*((f /. i) + (f /. j))*>) /. n = ((f ^ <*((f /. i) + (f /. j))*>) /. i) * ((f ^ <*((f /. i) + (f /. j))*>) /. j) or (f ^ <*((f /. i) + (f /. j))*>) /. n = ((f ^ <*((f /. i) + (f /. j))*>) /. i) + ((f ^ <*((f /. i) + (f /. j))*>) /. j) ) & i <> 0 & i < n & j <> 0 & j < n ) ) by A2, A4, A17; :: thesis: verum

end;

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

end;

len f <> 0 by A1;
then (len f) + (len <*((f /. i) + (f /. j))*>) <> 0 ;
then len (f ^ <*((f /. i) + (f /. j))*>) <> 0 by FINSEQ_1:22;
hence f ^ <*((f /. i) + (f /. j))*> is being_a_generation_from_squares by A7; :: thesis: verum