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
A3: 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 that
A4: n <> 0 and
A5: 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 ) )
A6: n <= (len f) + (len g) by A5, FINSEQ_1:22;
A7: now :: thesis: ( len f < n & 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 A8: 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
A9: n = (len f) + m by NAT_1:10;
(len f) + m <= (len f) + (len g) by A5, A9, FINSEQ_1:22;
then A10: m <= len g by XREAL_1:6;
A11: m <> 0 by A8, A9;
A12: m <= len g by A6, A9, XREAL_1:6;
A13: now :: thesis: ( ex k, l being Nat st
( ( g /. m = (g /. k) * (g /. l) or g /. m = (g /. k) + (g /. l) ) & k <> 0 & k < m & l <> 0 & l < m ) & 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 ) )
given k, l being Nat such that A14: ( g /. m = (g /. k) * (g /. l) or g /. m = (g /. k) + (g /. l) ) and
A15: k <> 0 and
A16: k < m and
A17: l <> 0 and
A18: 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 ) )
A19: ( (len f) + k <> 0 & (len f) + l <> 0 ) by A15, A17;
A20: ( (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
A21: now :: thesis: ( not g /. m = (g /. k) + (g /. l) or (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)) )
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 A9, A11, A10, Lm5
.= ((f ^ g) /. ((len f) + k)) + (g /. l) by A12, A15, A16, Lm5, XXREAL_0:2
.= ((f ^ g) /. ((len f) + k)) + ((f ^ g) /. ((len f) + l)) by A12, A17, A18, 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 :: thesis: ( not g /. m = (g /. k) * (g /. l) or (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)) )
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 A9, A11, A10, Lm5
.= ((f ^ g) /. ((len f) + k)) * (g /. l) by A12, A15, A16, Lm5, XXREAL_0:2
.= ((f ^ g) /. ((len f) + k)) * ((f ^ g) /. ((len f) + l)) by A12, A17, A18, 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 A14, A21; :: thesis: verum
end;
( (len f) + k < n & (len f) + l < n ) by A9, A16, A18, XREAL_1:6;
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 A20, A19; :: thesis: verum
end;
( 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 A9, A11, A10, Lm5;
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, A11, A10, A13; :: thesis: verum
end;
now :: thesis: ( n <= len f & 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 A22: 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 A23: (f ^ g) /. n = f /. n by A4, Lm4;
A24: now :: thesis: ( ex k, l being Nat st
( ( f /. n = (f /. k) * (f /. l) or f /. n = (f /. k) + (f /. l) ) & k <> 0 & k < n & l <> 0 & l < n ) & 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 ) )
given k, l being Nat such that A25: ( f /. n = (f /. k) * (f /. l) or f /. n = (f /. k) + (f /. l) ) and
A26: ( 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 ) )
( (f ^ g) /. k = f /. k & (f ^ g) /. l = f /. l ) by A22, A26, 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 A23, A25, A26; :: thesis: verum
end;
( 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, A22, Lm4;
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, A22, A24; :: 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 A7; :: thesis: verum
end;
len f <> 0 by A1;
then (len f) + (len g) <> 0 ;
then len (f ^ g) <> 0 by FINSEQ_1:22;
hence f ^ g is being_a_generation_from_squares by A3; :: thesis: verum