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 = & 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 ;
A6: len (x2 ^ y2) = (len x2) + (len y2) by FINSEQ_1:22;
then dom (x1 ^ y1) = dom (x2 ^ y2) by ;
then A7: dom (mlt ((x1 ^ y1),(x2 ^ y2))) = dom (x1 ^ y1) by ;
A8: multreal .: (y1,y2) = multreal * <:y1,y2:> by FUNCOP_1:def 3;
A9: dom multreal = 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 ;
dom y2 = Seg (len y1) by
.= dom y1 by FINSEQ_1:def 3 ;
then A11: dom (mlt (y1,y2)) = dom y1 by ;
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 ;
then A14: dom (multreal * <:x1,x2:>) = (dom x1) /\ (dom x2) by ;
A15: len (x1 ^ y1) = (len x1) + (len y1) by FINSEQ_1:22;
dom x2 = Seg (len x1) by
.= dom x1 by FINSEQ_1:def 3 ;
then A16: dom (mlt (x1,x2)) = dom x1 by ;
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 ;
then A21: i in dom (mlt ((x1 ^ y1),(x2 ^ y2))) by FINSEQ_1:def 3;
then i <= len (x1 ^ y1) by ;
then A22: (x1 ^ y1) /. i = (x1 ^ y1) . i by ;
i <= len (x2 ^ y2) by A1, A2, A15, A6, A4, A7, A21, FINSEQ_1:1;
then A23: (x2 ^ y2) /. i = (x2 ^ y2) . i by ;
A24: i <= (len x1) + (len y1) by ;
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 ;
then A28: (x2 ^ y2) . i = x2 . i by FINSEQ_1:def 7;
A29: i in dom (mlt (x1,x2)) by ;
then A30: ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i = (mlt (x1,x2)) . i by FINSEQ_1:def 7
.= (x1 /. i) * (x2 /. i) by ;
( x1 /. i = x1 . i & x2 /. i = x2 . i ) by ;
hence ((x1 ^ y1) /. i) * ((x2 ^ y2) /. i) = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i by ; :: 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 ;
i <= len (x1 ^ y1) by ;
then A33: (x1 ^ y1) /. i = (x1 ^ y1) . i by ;
set k = i -' (len x1);
A34: i -' (len x1) = i - (len x1) by ;
then A35: i = (len x1) + (i -' (len x1)) ;
i - (len x1) <= ((len x1) + (len y1)) - (len x1) by ;
then A36: i -' (len x1) <= len y1 by ;
i -' (len x1) > 0 by ;
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 ;
i = (len (mlt (x1,x2))) + (i -' (len x1)) by ;
then A40: ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i = (mlt (y1,y2)) . (i -' (len x1)) by
.= (y1 /. (i -' (len x1))) * (y2 /. (i -' (len x1))) by ;
i -' (len x1) in dom y1 by ;
then A41: (x1 ^ y1) . i = y1 . (i -' (len x1)) by ;
i -' (len x1) in Seg (len y1) by ;
then A42: i -' (len x1) in dom y2 by ;
( y1 /. (i -' (len x1)) = y1 . (i -' (len x1)) & y2 /. (i -' (len x1)) = y2 . (i -' (len x1)) ) by ;
hence ((x1 ^ y1) /. i) * ((x2 ^ y2) /. i) = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i by ; :: thesis: verum
end;
end;
end;
hence (mlt ((x1 ^ y1),(x2 ^ y2))) . i = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i by ; :: thesis: verum
end;
len (mlt ((x1 ^ y1),(x2 ^ y2))) = len (x1 ^ y1) by
.= (len x1) + (len y1) by FINSEQ_1:22 ;
then len (mlt ((x1 ^ y1),(x2 ^ y2))) = (len (mlt (x1,x2))) + (len (mlt (y1,y2))) by ;
hence mlt ((x1 ^ y1),(x2 ^ y2)) = (mlt (x1,x2)) ^ (mlt (y1,y2)) by ; :: thesis: verum