let i, j be Nat; :: thesis: for R being non empty doubleLoopStr
for f being FinSequence of R st f is being_an_Amalgam_of_squares & i <> 0 & i <= len f & j <> 0 & j <= len f holds
f ^ <*((f /. i) * (f /. j))*> is being_an_Amalgam_of_squares
let R be non empty doubleLoopStr ; :: thesis: for f being FinSequence of R st f is being_an_Amalgam_of_squares & i <> 0 & i <= len f & j <> 0 & j <= len f holds
f ^ <*((f /. i) * (f /. j))*> is being_an_Amalgam_of_squares
let f be FinSequence of R; :: thesis: ( f is being_an_Amalgam_of_squares & i <> 0 & i <= len f & j <> 0 & j <= len f implies f ^ <*((f /. i) * (f /. j))*> is being_an_Amalgam_of_squares )
assume that
A1: f is being_an_Amalgam_of_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_an_Amalgam_of_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_a_product_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) & 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_a_product_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) & 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_a_product_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) & 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_a_product_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) & 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_a_product_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) & i <> 0 & i < n & j <> 0 & j < n ) )
then A11: n <= len f by A6, NAT_1:13;

A12: now :: thesis: ( ex k, m being Nat st
( f /. n = (f /. k) * (f /. m) & k <> 0 & k < n & m <> 0 & m < n ) & not (f ^ <*((f /. i) * (f /. j))*>) /. n is being_a_product_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) & i <> 0 & i < n & j <> 0 & j < n ) )

given k, m being Nat such that A13: f /. n = (f /. k) * (f /. m) and
A14: ( k <> 0 & k < n ) and
A15: ( m <> 0 & m < n ) ; :: thesis: ( (f ^ <*((f /. i) * (f /. j))*>) /. n is being_a_product_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) & i <> 0 & i < n & j <> 0 & j < n ) )
(f ^ <*((f /. i) * (f /. j))*>) /. n = (f /. k) * (f /. m) by A8, A11, A13, Lm4
.= ((f ^ <*((f /. i) * (f /. j))*>) /. k) * (f /. m) by A11, A14, Lm4, XXREAL_0:2
.= ((f ^ <*((f /. i) * (f /. j))*>) /. k) * ((f ^ <*((f /. i) * (f /. j))*>) /. m) by A11, A15, Lm4, XXREAL_0:2 ;
hence ( (f ^ <*((f /. i) * (f /. j))*>) /. n is being_a_product_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) & i <> 0 & i < n & j <> 0 & j < n ) ) by A14, A15; :: thesis: verum

end;

( f /. n is being_a_product_of_squares & not (f ^ <*((f /. i) * (f /. j))*>) /. n is being_a_product_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) & i <> 0 & i < n & j <> 0 & j < n ) ) by A8, A11, Lm4;
hence ( (f ^ <*((f /. i) * (f /. j))*>) /. n is being_a_product_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) & i <> 0 & i < n & j <> 0 & j < n ) ) by A1, A8, A11, A12; :: thesis: verum

end;

now :: thesis: ( n = len (f ^ <*((f /. i) * (f /. j))*>) & not (f ^ <*((f /. i) * (f /. j))*>) /. n is being_a_product_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) & 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_a_product_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) & 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_a_product_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) & i <> 0 & i < n & j <> 0 & j < n ) ) by A2, A4, A17; :: thesis: verum

end;

hence ( (f ^ <*((f /. i) * (f /. j))*>) /. n is being_a_product_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) & 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_an_Amalgam_of_squares by A7; :: thesis: verum