let G be non empty multLoopStr ; :: thesis: for x1, x2, y1, y2 being FinSequence of G st len x1 = len x2 & len y1 = len y2 holds
mlt ((x1 ^ y1),(x2 ^ y2)) = (mlt (x1,x2)) ^ (mlt (y1,y2))
let x1, x2, y1, y2 be FinSequence of G; :: 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: the multF of G .: ((x1 ^ y1),(x2 ^ y2)) = the multF of G * <:(x1 ^ y1),(x2 ^ y2):> by FUNCOP_1:def 3;
A4: dom (x1 ^ y1) = Seg (len (x1 ^ y1)) by FINSEQ_1:def 3;
A5: rng (x2 ^ y2) c= the carrier of G by FINSEQ_1:def 4;
( dom the multF of G = [: the carrier of G, the carrier of G:] & rng (x1 ^ y1) c= the carrier of G ) by FINSEQ_1:def 4, FUNCT_2:def 1;
then [:(rng (x1 ^ y1)),(rng (x2 ^ y2)):] c= dom the multF of G by A5, ZFMISC_1:96;
then A6: dom ( the multF of G * <:(x1 ^ y1),(x2 ^ y2):>) = (dom (x1 ^ y1)) /\ (dom (x2 ^ y2)) by A3, FUNCOP_1:69;
A7: len (x2 ^ y2) = (len x2) + (len y2) by FINSEQ_1:22;
dom (x2 ^ y2) = Seg (len (x2 ^ y2)) by FINSEQ_1:def 3;
then dom (x1 ^ y1) = dom (x2 ^ y2) by A1, A2, A7, A4, FINSEQ_1:22;
then A8: dom (mlt ((x1 ^ y1),(x2 ^ y2))) = dom (x1 ^ y1) by A3, A6, FVSUM_1:def 7;
A9: the multF of G .: (y1,y2) = the multF of G * <:y1,y2:> by FUNCOP_1:def 3;
A10: dom the multF of G = [: the carrier of G, the carrier of G:] by FUNCT_2:def 1;
( rng y1 c= the carrier of G & rng y2 c= the carrier of G ) by FINSEQ_1:def 4;
then [:(rng y1),(rng y2):] c= dom the multF of G by A10, ZFMISC_1:96;
then A11: dom ( the multF of G * <:y1,y2:>) = (dom y1) /\ (dom y2) by A9, FUNCOP_1:69;
dom y2 = Seg (len y1) by A2, FINSEQ_1:def 3
.= dom y1 by FINSEQ_1:def 3 ;
then A12: dom (mlt (y1,y2)) = dom y1 by A9, A11, FVSUM_1:def 7;
then dom (mlt (y1,y2)) = Seg (len y1) by FINSEQ_1:def 3;
then A13: len (mlt (y1,y2)) = len y1 by FINSEQ_1:def 3;
A14: the multF of G .: (x1,x2) = the multF of G * <:x1,x2:> by FUNCOP_1:def 3;
( rng x1 c= the carrier of G & rng x2 c= the carrier of G ) by FINSEQ_1:def 4;
then [:(rng x1),(rng x2):] c= dom the multF of G by A10, ZFMISC_1:96;
then A15: dom ( the multF of G * <:x1,x2:>) = (dom x1) /\ (dom x2) by A14, FUNCOP_1:69;
A16: 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 A17: dom (mlt (x1,x2)) = dom x1 by A14, A15, FVSUM_1:def 7;
then A18: dom (mlt (x1,x2)) = Seg (len x1) by FINSEQ_1:def 3;
A19: 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
A20: 1 <= i and
A21: 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 A20, A21, FINSEQ_1:1;
then A22: i in dom (mlt ((x1 ^ y1),(x2 ^ y2))) by FINSEQ_1:def 3;
then i <= len (x1 ^ y1) by A4, A8, FINSEQ_1:1;
then A23: (x1 ^ y1) /. i = (x1 ^ y1) . i by A20, FINSEQ_4:15;
i <= len (x2 ^ y2) by A1, A2, A16, A7, A4, A8, A22, FINSEQ_1:1;
then A24: (x2 ^ y2) /. i = (x2 ^ y2) . i by A20, FINSEQ_4:15;
A25: i <= (len x1) + (len y1) by A16, A4, A8, A22, 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 A26: i <= len x1 ; :: thesis: ((x1 ^ y1) /. i) * ((x2 ^ y2) /. i) = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i

then A27: i in Seg (len x1) by A20, FINSEQ_1:1;
then A28: i in dom x1 by FINSEQ_1:def 3;
i in dom x2 by A1, A27, FINSEQ_1:def 3;
then A29: (x2 ^ y2) . i = x2 . i by FINSEQ_1:def 7;
A30: i in dom (mlt (x1,x2)) by A17, A27, FINSEQ_1:def 3;
then A31: ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i = (mlt (x1,x2)) . i by FINSEQ_1:def 7
.= (x1 /. i) * (x2 /. i) by A30, Th4 ;
( x1 /. i = x1 . i & x2 /. i = x2 . i ) by A1, A20, A26, FINSEQ_4:15;
hence ((x1 ^ y1) /. i) * ((x2 ^ y2) /. i) = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i by A23, A24, A28, A29, A31, FINSEQ_1:def 7; :: thesis: verum

end;

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

i <= len (x2 ^ y2) by A1, A2, A16, A7, A4, A8, A22, FINSEQ_1:1;
then A33: (x2 ^ y2) /. i = (x2 ^ y2) . i by A20, FINSEQ_4:15;
i <= len (x1 ^ y1) by A4, A8, A22, FINSEQ_1:1;
then A34: (x1 ^ y1) /. i = (x1 ^ y1) . i by A20, FINSEQ_4:15;
set k = i -' (len x1);
A35: i -' (len x1) = i - (len x1) by A32, XREAL_1:233;
then A36: i = (len x1) + (i -' (len x1)) ;
i - (len x1) <= ((len x1) + (len y1)) - (len x1) by A25, XREAL_1:13;
then A37: i -' (len x1) <= len y1 by A32, XREAL_1:233;
i -' (len x1) > 0 by A32, A35, XREAL_1:50;
then A38: 0 + 1 <= i -' (len x1) by NAT_1:13;
then A39: i -' (len x1) in Seg (len y1) by A37, FINSEQ_1:1;
then A40: i -' (len x1) in dom (mlt (y1,y2)) by A12, FINSEQ_1:def 3;
i = (len (mlt (x1,x2))) + (i -' (len x1)) by A18, A36, FINSEQ_1:def 3;
then A41: ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i = (mlt (y1,y2)) . (i -' (len x1)) by A40, FINSEQ_1:def 7
.= (y1 /. (i -' (len x1))) * (y2 /. (i -' (len x1))) by A40, Th4 ;
i -' (len x1) in dom y1 by A39, FINSEQ_1:def 3;
then A42: (x1 ^ y1) . i = y1 . (i -' (len x1)) by A36, FINSEQ_1:def 7;
i -' (len x1) in Seg (len y1) by A38, A37, FINSEQ_1:1;
then A43: 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, A38, A37, FINSEQ_4:15;
hence ((x1 ^ y1) /. i) * ((x2 ^ y2) /. i) = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i by A1, A36, A43, A42, A34, A33, A41, FINSEQ_1:def 7; :: thesis: verum

end;

end;

end;

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

end;

len (mlt ((x1 ^ y1),(x2 ^ y2))) = len (x1 ^ y1) by A4, A8, 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 A18, A13, FINSEQ_1:def 3;
then len (mlt ((x1 ^ y1),(x2 ^ y2))) = len ((mlt (x1,x2)) ^ (mlt (y1,y2))) by FINSEQ_1:22;
hence mlt ((x1 ^ y1),(x2 ^ y2)) = (mlt (x1,x2)) ^ (mlt (y1,y2)) by A19, FINSEQ_1:14; :: thesis: verum