let G be non empty multLoopStr ; 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; ( 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
; 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;
( 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)))
;
(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 ((x1 ^ y1) /. i) * ((x2 ^ y2) /. i) = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . iper cases
( i <= len x1 or i > len x1 )
;
suppose A26:
i <= len x1
;
((x1 ^ y1) /. i) * ((x2 ^ y2) /. i) = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . ithen 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;
verum end; suppose A32:
i > len x1
;
((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;
verum end;
hence
(mlt ((x1 ^ y1),(x2 ^ y2))) . i = ((mlt (x1,x2)) ^ (mlt (y1,y2))) . i
by A22, Th4;
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; verum