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) ^ <*((f /. (len f)) * (g /. (len 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) ^ <*((f /. (len f)) * (g /. (len g)))*> is being_an_Amalgam_of_squares )
assume that
A1: f is being_an_Amalgam_of_squares and
A2: g is being_an_Amalgam_of_squares ; :: thesis: (f ^ g) ^ <*((f /. (len f)) * (g /. (len g)))*> is being_an_Amalgam_of_squares
A3: ( len f <> 0 & len f <= len f ) by A1, Def10;
( len f <> 0 & len f <= (len f) + (len g) ) by A1, Def10, NAT_1:11;
then A4: ( len f <> 0 & len f <= len (f ^ g) ) by FINSEQ_1:35;
A5: ( len g <> 0 & len g <= len g ) by A2, Def10;
then A6: ( (len f) + (len g) <> 0 & (len f) + (len g) <= len (f ^ g) ) by FINSEQ_1:35, NAT_1:7;
A7: (f ^ g) /. (len f) = f /. (len f) by A3, Lm4;
A8: (f ^ g) /. ((len f) + (len g)) = g /. (len g) by A5, Lm5;
f ^ g is being_an_Amalgam_of_squares by A1, A2, Lm80;
hence (f ^ g) ^ <*((f /. (len f)) * (g /. (len g)))*> is being_an_Amalgam_of_squares by A4, A6, A7, A8, Lm81; :: thesis: verum