let x1, x2, y1, y2 be FinSequence of REAL ; :: thesis: ( len x1 = len x2 & len y1 = len y2 implies mlt ((x1 ^ y1),(x2 ^ y2)) = (mlt (x1,x2)) ^ (mlt (y1,y2)) )
assume that
A1: len x1 = len x2 and
A2: len y1 = len y2 ; :: thesis: mlt ((x1 ^ y1),(x2 ^ y2)) = (mlt (x1,x2)) ^ (mlt (y1,y2))
A3: multreal .: ((x1 ^ y1),(x2 ^ y2)) = multreal * <:(x1 ^ y1),(x2 ^ y2):> by FUNCOP_1:def 3;
A4: dom (x1 ^ y1) = Seg (len (x1 ^ y1)) by FINSEQ_1:def 3;
( dom multreal = [:REAL,REAL:] & rng (x1 ^ y1) c= REAL ) by FUNCT_2:def 1;
then [:(rng (x1 ^ y1)),(rng (x2 ^ y2)):] c= dom multreal by ZFMISC_1:96;
then A5: dom (multreal * <:(x1 ^ y1),(x2 ^ y2):>) = (dom (x1 ^ y1)) /\ (dom (x2 ^ y2)) by A3, FUNCOP_1:69;
A6: len (x2 ^ y2) = (len x2) + (len y2) by FINSEQ_1:22;
then dom (x1 ^ y1) = dom (x2 ^ y2) by A1, A2, A4, FINSEQ_1:22, FINSEQ_1:def 3;
then A7: dom (mlt ((x1 ^ y1),(x2 ^ y2))) = dom (x1 ^ y1) by A3, A5, RVSUM_1:def 9;
A8: multreal .: (y1,y2) = multreal * <:y1,y2:> by FUNCOP_1:def 3;
A9: dom multreal = [:REAL,REAL:] by FUNCT_2:def 1;
then [:(rng y1),(rng y2):] c= dom multreal by ZFMISC_1:96;
then A10: dom (multreal * <:y1,y2:>) = (dom y1) /\ (dom y2) by A8, FUNCOP_1:69;
dom y2 = Seg (len y1) by A2, FINSEQ_1:def 3
.= dom y1 by FINSEQ_1:def 3 ;
then A11: dom (mlt (y1,y2)) = dom y1 by A8, A10, RVSUM_1:def 9;
then dom (mlt (y1,y2)) = Seg (len y1) by FINSEQ_1:def 3;
then A12: len (mlt (y1,y2)) = len y1 by FINSEQ_1:def 3;
A13: multreal .: (x1,x2) = multreal * <:x1,x2:> by FUNCOP_1:def 3;
[:(rng x1),(rng x2):] c= dom multreal by A9, ZFMISC_1:96;
then A14: dom (multreal * <:x1,x2:>) = (dom x1) /\ (dom x2) by A13, FUNCOP_1:69;
A15: len (x1 ^ y1) = (len x1) + (len y1) by FINSEQ_1:22;
dom x2 = Seg (len x1) by A1, FINSEQ_1:def 3
.= dom x1 by FINSEQ_1:def 3 ;
then A16: dom (mlt (x1,x2)) = dom x1 by A13, A14, RVSUM_1:def 9;
then A17: dom (mlt (x1,x2)) = Seg (len x1) by FINSEQ_1:def 3;
A18: for i being Nat st 1 <= i & i <= len (mlt ((x1 ^ y1),(x2 ^ y2))) holds
(mlt ((x1 ^ y1),(x2 ^ y2))) . i = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (mlt ((x1 ^ y1),(x2 ^ y2))) implies (mlt ((x1 ^ y1),(x2 ^ y2))) . i = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i )
assume that
A19: 1 <= i and
A20: i <= len (mlt ((x1 ^ y1),(x2 ^ y2))) ; :: thesis: (mlt ((x1 ^ y1),(x2 ^ y2))) . i = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i
i in Seg (len (mlt ((x1 ^ y1),(x2 ^ y2)))) by A19, A20;
then A21: i in dom (mlt ((x1 ^ y1),(x2 ^ y2))) by FINSEQ_1:def 3;
then i <= len (x1 ^ y1) by A4, A7, FINSEQ_1:1;
then A22: (x1 ^ y1) /. i = (x1 ^ y1) . i by A19, FINSEQ_4:15;
i <= len (x2 ^ y2) by A1, A2, A15, A6, A4, A7, A21, FINSEQ_1:1;
then A23: (x2 ^ y2) /. i = (x2 ^ y2) . i by A19, FINSEQ_4:15;
A24: i <= (len x1) + (len y1) by A15, A4, A7, A21, FINSEQ_1:1;

now :: thesis: ((x1 ^ y1) /. i) * ((x2 ^ y2) /. i) = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i

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

suppose A25: i <= len x1 ; :: thesis: ((x1 ^ y1) /. i) * ((x2 ^ y2) /. i) = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i

then A26: i in Seg (len x1) by A19;
then A27: i in dom x1 by FINSEQ_1:def 3;
i in dom x2 by A1, A26, FINSEQ_1:def 3;
then A28: (x2 ^ y2) . i = x2 . i by FINSEQ_1:def 7;
A29: i in dom (mlt (x1,x2)) by A16, A26, FINSEQ_1:def 3;
then A30: ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i = (mlt (x1,x2)) . i by FINSEQ_1:def 7
.= (x1 /. i) * (x2 /. i) by A29, Th13 ;
( x1 /. i = x1 . i & x2 /. i = x2 . i ) by A1, A19, A25, FINSEQ_4:15;
hence ((x1 ^ y1) /. i) * ((x2 ^ y2) /. i) = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i by A22, A23, A27, A28, A30, FINSEQ_1:def 7; :: thesis: verum

end;

suppose A31: i > len x1 ; :: thesis: ((x1 ^ y1) /. i) * ((x2 ^ y2) /. i) = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i

i <= len (x2 ^ y2) by A1, A2, A15, A6, A4, A7, A21, FINSEQ_1:1;
then A32: (x2 ^ y2) /. i = (x2 ^ y2) . i by A19, FINSEQ_4:15;
i <= len (x1 ^ y1) by A4, A7, A21, FINSEQ_1:1;
then A33: (x1 ^ y1) /. i = (x1 ^ y1) . i by A19, FINSEQ_4:15;
set k = i -' (len x1);
A34: i -' (len x1) = i - (len x1) by A31, XREAL_1:233;
then A35: i = (len x1) + (i -' (len x1)) ;
i - (len x1) <= ((len x1) + (len y1)) - (len x1) by A24, XREAL_1:13;
then A36: i -' (len x1) <= len y1 by A31, XREAL_1:233;
i -' (len x1) > 0 by A31, A34, XREAL_1:50;
then (i -' (len x1)) + 1 > 0 + 1 by XREAL_1:6;
then A37: 1 <= i -' (len x1) by NAT_1:13;
then A38: i -' (len x1) in Seg (len y1) by A36;
then A39: i -' (len x1) in dom (mlt (y1,y2)) by A11, FINSEQ_1:def 3;
i = (len (mlt (x1,x2))) + (i -' (len x1)) by A17, A35, FINSEQ_1:def 3;
then A40: ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i = (mlt (y1,y2)) . (i -' (len x1)) by A39, FINSEQ_1:def 7
.= (y1 /. (i -' (len x1))) * (y2 /. (i -' (len x1))) by A39, Th13 ;
i -' (len x1) in dom y1 by A38, FINSEQ_1:def 3;
then A41: (x1 ^ y1) . i = y1 . (i -' (len x1)) by A35, FINSEQ_1:def 7;
i -' (len x1) in Seg (len y1) by A37, A36;
then A42: i -' (len x1) in dom y2 by A2, FINSEQ_1:def 3;
( y1 /. (i -' (len x1)) = y1 . (i -' (len x1)) & y2 /. (i -' (len x1)) = y2 . (i -' (len x1)) ) by A2, A37, A36, FINSEQ_4:15;
hence ((x1 ^ y1) /. i) * ((x2 ^ y2) /. i) = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i by A1, A35, A42, A41, A33, A32, A40, FINSEQ_1:def 7; :: thesis: verum

end;

end;

end;

hence (mlt ((x1 ^ y1),(x2 ^ y2))) . i = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i by A21, Th13; :: thesis: verum

end;

len (mlt ((x1 ^ y1),(x2 ^ y2))) = len (x1 ^ y1) by A4, A7, FINSEQ_1:def 3
.= (len x1) + (len y1) by FINSEQ_1:22 ;
then len (mlt ((x1 ^ y1),(x2 ^ y2))) = (len (mlt (x1,x2))) + (len (mlt (y1,y2))) by A17, A12, FINSEQ_1:def 3;
hence mlt ((x1 ^ y1),(x2 ^ y2)) = (mlt (x1,x2)) ^ (mlt (y1,y2)) by A18, FINSEQ_1:22; :: thesis: verum