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
len f <> 0 by A1;
then A3: ( (len f) + (len g) <= len (f ^ g) & (f ^ g) /. (len f) = f /. (len f) ) by Lm4, FINSEQ_1:22;
len g <> 0 by A2;
then A4: ( (len f) + (len g) <> 0 & (f ^ g) /. ((len f) + (len g)) = g /. (len g) ) by Lm5;
len f <= (len f) + (len g) by NAT_1:11;
then A5: len f <= len (f ^ g) by FINSEQ_1:22;
( len f <> 0 & 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 A5, A3, A4, Lm81; :: thesis: verum