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

.= (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

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

len (mlt ((x1 ^ y1),(x2 ^ y2))) =
len (x1 ^ y1)
by A4, A7, FINSEQ_1:def 3
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;

end;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))) . iend;

hence
(mlt ((x1 ^ y1),(x2 ^ y2))) . i = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i
by A21, Th13; :: thesis: verumper cases
( i <= len x1 or i > len x1 )
;

end;

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;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

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;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

.= (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