let G be non empty multLoopStr ; for x1, x2 being FinSequence of G
for i being Element of NAT st i in dom (mlt (x1,x2)) holds
( (mlt (x1,x2)) . i = (x1 /. i) * (x2 /. i) & (mlt (x1,x2)) /. i = (x1 /. i) * (x2 /. i) )
let x1, x2 be FinSequence of G; for i being Element of NAT st i in dom (mlt (x1,x2)) holds
( (mlt (x1,x2)) . i = (x1 /. i) * (x2 /. i) & (mlt (x1,x2)) /. i = (x1 /. i) * (x2 /. i) )
let i be Element of NAT ; ( i in dom (mlt (x1,x2)) implies ( (mlt (x1,x2)) . i = (x1 /. i) * (x2 /. i) & (mlt (x1,x2)) /. i = (x1 /. i) * (x2 /. i) ) )
assume A1:
i in dom (mlt (x1,x2))
; ( (mlt (x1,x2)) . i = (x1 /. i) * (x2 /. i) & (mlt (x1,x2)) /. i = (x1 /. i) * (x2 /. i) )
A2:
mlt (x1,x2) = the multF of G .: (x1,x2)
by FVSUM_1:def 7;
A3:
rng x2 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 c= the carrier of G )
by FINSEQ_1:def 4, FUNCT_2:def 1;
then
[:(rng x1),(rng x2):] c= dom the multF of G
by A3, ZFMISC_1:96;
then A4:
dom (mlt (x1,x2)) = (dom x1) /\ (dom x2)
by A2, FUNCOP_1:69;
then
i in dom x2
by A1, XBOOLE_0:def 4;
then A5:
x2 /. i = x2 . i
by PARTFUN1:def 6;
i in dom x1
by A1, A4, XBOOLE_0:def 4;
then
x1 /. i = x1 . i
by PARTFUN1:def 6;
hence
(mlt (x1,x2)) . i = (x1 /. i) * (x2 /. i)
by A1, A5, FVSUM_1:60; (mlt (x1,x2)) /. i = (x1 /. i) * (x2 /. i)
hence
(mlt (x1,x2)) /. i = (x1 /. i) * (x2 /. i)
by A1, PARTFUN1:def 6; verum