let G be non empty multLoopStr ; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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) ; :: thesis: ( (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:119;
then A4: dom (mlt x1,x2) = (dom x1) /\ (dom x2) by A2, FUNCOP_1:84;
then i in dom x2 by A1, XBOOLE_0:def 4;
then A5: x2 /. i = x2 . i by PARTFUN1:def 8;
i in dom x1 by A1, A4, XBOOLE_0:def 4;
then x1 /. i = x1 . i by PARTFUN1:def 8;
hence (mlt x1,x2) . i = (x1 /. i) * (x2 /. i) by A1, A5, FVSUM_1:73; :: thesis: (mlt x1,x2) /. i = (x1 /. i) * (x2 /. i)
hence (mlt x1,x2) /. i = (x1 /. i) * (x2 /. i) by A1, PARTFUN1:def 8; :: thesis: verum