let L be non empty right_complementable add-associative right_zeroed distributive unital doubleLoopStr ; :: thesis: for z1, z2 being FinSequence of the carrier of L
for f1, f2 being NAT -valued FinSequence st len f1 = len z1 & len f2 <= len z2 holds
rpoly ((f1 ^ f2),(z1 ^ z2)) = (rpoly (f1,z1)) ^ (rpoly (f2,z2))
let z1, z2 be FinSequence of the carrier of L; :: thesis: for f1, f2 being NAT -valued FinSequence st len f1 = len z1 & len f2 <= len z2 holds
rpoly ((f1 ^ f2),(z1 ^ z2)) = (rpoly (f1,z1)) ^ (rpoly (f2,z2))
let f1, f2 be NAT -valued FinSequence; :: thesis: ( len f1 = len z1 & len f2 <= len z2 implies rpoly ((f1 ^ f2),(z1 ^ z2)) = (rpoly (f1,z1)) ^ (rpoly (f2,z2)) )
assume A1: ( len f1 = len z1 & len f2 <= len z2 ) ; :: thesis: rpoly ((f1 ^ f2),(z1 ^ z2)) = (rpoly (f1,z1)) ^ (rpoly (f2,z2))
A2: ( len (rpoly ((f1 ^ f2),(z1 ^ z2))) = len (f1 ^ f2) & len (f1 ^ f2) = (len f1) + (len f2) & len ((rpoly (f1,z1)) ^ (rpoly (f2,z2))) = (len (rpoly (f1,z1))) + (len (rpoly (f2,z2))) ) by Def1, FINSEQ_1:22;
A3: ( len (rpoly (f1,z1)) = len f1 & len (rpoly (f2,z2)) = len f2 ) by Def1;
for i being Nat st 1 <= i & i <= len (rpoly ((f1 ^ f2),(z1 ^ z2))) holds
(rpoly ((f1 ^ f2),(z1 ^ z2))) . i = ((rpoly (f1,z1)) ^ (rpoly (f2,z2))) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (rpoly ((f1 ^ f2),(z1 ^ z2))) implies (rpoly ((f1 ^ f2),(z1 ^ z2))) . i = ((rpoly (f1,z1)) ^ (rpoly (f2,z2))) . i )
assume A4: ( 1 <= i & i <= len (rpoly ((f1 ^ f2),(z1 ^ z2))) ) ; :: thesis: (rpoly ((f1 ^ f2),(z1 ^ z2))) . i = ((rpoly (f1,z1)) ^ (rpoly (f2,z2))) . i
A5: ( (len f1) + (len f2) <= (len z1) + (len z2) & (len z1) + (len z2) = len (z1 ^ z2) ) by A1, FINSEQ_1:22, XREAL_1:6;
then i <= len (z1 ^ z2) by A2, A4, XXREAL_0:2;
then ( i in dom (f1 ^ f2) & i in dom (z1 ^ z2) ) by A2, A4, FINSEQ_3:25;
then A6: ( (f1 ^ f2) /. i = (f1 ^ f2) . i & (z1 ^ z2) /. i = (z1 ^ z2) . i ) by PARTFUN1:def 6;

per cases ( i <= len f1 or i > len f1 ) ;

suppose A7: i <= len f1 ; :: thesis: (rpoly ((f1 ^ f2),(z1 ^ z2))) . i = ((rpoly (f1,z1)) ^ (rpoly (f2,z2))) . i

then A8: ( i in dom f1 & i in dom z1 & i in dom (rpoly (f1,z1)) ) by A1, A3, A4, FINSEQ_3:25;
then A9: ((rpoly (f1,z1)) ^ (rpoly (f2,z2))) . i = (rpoly (f1,z1)) . i by FINSEQ_1:def 7
.= rpoly ((f1 /. i),(z1 /. i)) by A4, A7, Def1 ;
( f1 /. i = f1 . i & f1 . i = (f1 ^ f2) . i & z1 /. i = z1 . i & z1 . i = (z1 ^ z2) . i ) by A8, PARTFUN1:def 6, FINSEQ_1:def 7;
hence (rpoly ((f1 ^ f2),(z1 ^ z2))) . i = ((rpoly (f1,z1)) ^ (rpoly (f2,z2))) . i by A6, A2, A4, Def1, A9; :: thesis: verum

end;

suppose A10: i > len f1 ; :: thesis: (rpoly ((f1 ^ f2),(z1 ^ z2))) . i = ((rpoly (f1,z1)) ^ (rpoly (f2,z2))) . i

then reconsider I = i - (len f1) as Nat by NAT_1:21;
( I + (len f1) <= (len f1) + (len f2) & I <> 0 ) by A2, A10, A4;
then A11: ( 1 <= I & I <= len f2 ) by XREAL_1:6, NAT_1:14;
then I <= len z2 by A1, XXREAL_0:2;
then A12: ( I in dom f2 & I in dom z2 ) by A11, FINSEQ_3:25;
A13: ((rpoly (f1,z1)) ^ (rpoly (f2,z2))) . i = (rpoly (f2,z2)) . I by A2, A3, A10, A4, FINSEQ_1:24
.= rpoly ((f2 /. I),(z2 /. I)) by A11, Def1 ;
( len z1 < i & i <= len (z1 ^ z2) ) by A1, A10, A2, A4, A5, XXREAL_0:2;
then ( f2 /. I = f2 . I & f2 . I = (f1 ^ f2) . i & z2 /. I = z2 . I & z2 . I = (z1 ^ z2) . i ) by A1, A2, A12, A4, PARTFUN1:def 6, FINSEQ_1:24;
hence (rpoly ((f1 ^ f2),(z1 ^ z2))) . i = ((rpoly (f1,z1)) ^ (rpoly (f2,z2))) . i by A6, A2, A4, Def1, A13; :: thesis: verum

end;

end;

end;

hence rpoly ((f1 ^ f2),(z1 ^ z2)) = (rpoly (f1,z1)) ^ (rpoly (f2,z2)) by A2, A3, FINSEQ_1:14; :: thesis: verum