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 A1: ( f is being_an_Amalgam_of_squares & i <> 0 & i <= len f & j <> 0 & j <= len f ) ; :: thesis: f ^ <*((f /. i) * (f /. j))*> is being_an_Amalgam_of_squares
then len f <> 0 by Def10;
then (len f) + (len <*((f /. i) * (f /. j))*>) <> 0 by NAT_1:7;
then A2: len (f ^ <*((f /. i) * (f /. j))*>) <> 0 by FINSEQ_1:35;
set g = f ^ <*((f /. i) * (f /. j))*>;
A3: len (f ^ <*((f /. i) * (f /. j))*>) = (len f) + (len <*((f /. i) * (f /. j))*>) by FINSEQ_1:35
.= (len f) + 1 by Lm2 ;
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 A4: ( n <> 0 & 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 ) )

A5: now

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 A6: n <= len f by A3, NAT_1:13;
then A7: ( 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 A4, Lm4;

now

given k, m being Nat such that A8: ( f /. n = (f /. k) * (f /. m) & k <> 0 & k < n & 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 A4, A6, A8, Lm4
.= ((f ^ <*((f /. i) * (f /. j))*>) /. k) * (f /. m) by A6, A8, Lm4, XXREAL_0:2
.= ((f ^ <*((f /. i) * (f /. j))*>) /. k) * ((f ^ <*((f /. i) * (f /. j))*>) /. m) by A6, A8, 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 A8; :: 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 A1, A4, A6, A7, Def10; :: thesis: verum

end;

now

assume 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 ) )
then (f ^ <*((f /. i) * (f /. j))*>) /. n = (f /. i) * (f /. j) by A3, Lm3
.= ((f ^ <*((f /. i) * (f /. j))*>) /. i) * (f /. j) by A1, Lm4
.= ((f ^ <*((f /. i) * (f /. j))*>) /. i) * ((f ^ <*((f /. i) * (f /. j))*>) /. j) by A1, Lm4 ;
then ( (f ^ <*((f /. i) * (f /. j))*>) /. n = ((f ^ <*((f /. i) * (f /. j))*>) /. i) * ((f ^ <*((f /. i) * (f /. j))*>) /. j) & i < n & j < n ) by A1, A3, A9, NAT_1:13;
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; :: 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 A4, A5, XXREAL_0:1; :: thesis: verum

end;

hence f ^ <*((f /. i) * (f /. j))*> is being_an_Amalgam_of_squares by A2, Def10; :: thesis: verum