let R be non empty doubleLoopStr ; :: thesis: for f, g being FinSequence of R st f is being_an_Amalgam_of_squares & g is being_an_Amalgam_of_squares holds
f ^ g is being_an_Amalgam_of_squares
let f, g be FinSequence of R; :: thesis: ( f is being_an_Amalgam_of_squares & g is being_an_Amalgam_of_squares implies f ^ g is being_an_Amalgam_of_squares )
assume A1: ( f is being_an_Amalgam_of_squares & g is being_an_Amalgam_of_squares ) ; :: thesis: f ^ g is being_an_Amalgam_of_squares
then len f <> 0 by Def10;
then (len f) + (len g) <> 0 by NAT_1:7;
then A2: 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_a_product_of_squares holds
ex i, j being Nat st
( (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_a_product_of_squares implies ex i, j being Nat st
( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) & i <> 0 & i < n & j <> 0 & j < n ) )
assume A3: ( n <> 0 & n <= len (f ^ g) ) ; :: thesis: ( (f ^ g) /. n is being_a_product_of_squares or ex i, j being Nat st
( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) & i <> 0 & i < n & j <> 0 & j < n ) )
then A4: n <= (len f) + (len g) by FINSEQ_1:35;

A5: now

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

now

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

end;

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

end;

now

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

now

given k, l being Nat such that A14: ( g /. m = (g /. k) * (g /. l) & k <> 0 & k < m & l <> 0 & l < m ) ; :: thesis: ( (f ^ g) /. n is being_a_product_of_squares or ex i, j being Nat st
( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) & i <> 0 & i < n & j <> 0 & j < n ) )
A15: (f ^ g) /. n = (g /. k) * (g /. l) by A10, A12, A14, Lm5
.= ((f ^ g) /. ((len f) + k)) * (g /. l) by A11, A14, Lm5, XXREAL_0:2
.= ((f ^ g) /. ((len f) + k)) * ((f ^ g) /. ((len f) + l)) by A11, A14, Lm5, XXREAL_0:2 ;
A16: ( (len f) + k <> 0 & (len f) + l <> 0 ) by A14, NAT_1:7;
( (len f) + k < n & (len f) + l < n ) by A10, A14, XREAL_1:8;
hence ( (f ^ g) /. n is being_a_product_of_squares or ex i, j being Nat st
( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) & i <> 0 & i < n & j <> 0 & j < n ) ) by A15, A16; :: thesis: verum

end;

hence ( (f ^ g) /. n is being_a_product_of_squares or ex i, j being Nat st
( (f ^ g) /. n = ((f ^ g) /. i) * ((f ^ g) /. j) & i <> 0 & i < n & j <> 0 & j < n ) ) by A1, A12, A13, Def10; :: thesis: verum

end;

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

end;

hence f ^ g is being_an_Amalgam_of_squares by A2, Def10; :: thesis: verum