per cases ( ( f is empty & g is empty ) or not f is empty or not g is empty ) ;

suppose ( f is empty & g is empty ) ; :: thesis: for b₁ being FinSequence of E st b₁ = f ^ g holds
b₁ is P -quadratic

hence for b₁ being FinSequence of E st b₁ = f ^ g holds
b₁ is P -quadratic by FINSEQ_1:34; :: thesis: verum

end;

suppose L: ( not f is empty or not g is empty ) ; :: thesis: for b₁ being FinSequence of E st b₁ = f ^ g holds
b₁ is P -quadratic

now :: thesis: for i being Element of dom (f ^ g) ex a being non zero Element of E ex b being Element of E st
( a in P & (f ^ g) . i = a * (b ^2) )

let i be Element of dom (f ^ g); :: thesis: ex a being non zero Element of E ex b being Element of E st
( b in P & (f ^ g) . a = b * (b₃ ^2) )

per cases ( i in dom f or ex n being Nat st
( n in dom g & i = (len f) + n ) ) by L, FINSEQ_1:25;

suppose B: i in dom f ; :: thesis: ex a being non zero Element of E ex b being Element of E st
( b in P & (f ^ g) . a = b * (b₃ ^2) )

then ( (f ^ g) . i = f . i & f is P -quadratic ) by FINSEQ_1:def 7;
hence ex a being non zero Element of E ex b being Element of E st
( a in P & (f ^ g) . i = a * (b ^2) ) by B; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom g & i = (len f) + n ) ; :: thesis: ex a being non zero Element of E ex b being Element of E st
( b in P & (f ^ g) . a = b * (b₃ ^2) )

then consider n being Nat such that
A: ( n in dom g & i = (len f) + n ) ;
( (f ^ g) . i = g . n & g is P -quadratic ) by A, FINSEQ_1:def 7;
hence ex a being non zero Element of E ex b being Element of E st
( a in P & (f ^ g) . i = a * (b ^2) ) by A; :: thesis: verum

end;

end;

end;

hence for b₁ being FinSequence of E st b₁ = f ^ g holds
b₁ is P -quadratic ; :: thesis: verum

end;

end;