let G be non empty multLoopStr ; :: thesis:
let x1, x2 be FinSequence of G; :: thesis:
let i be Element of NAT ; :: thesis:
assume A1: i in dom (mlt x1,x2) ; :: thesis:
A4: dom the multF of G = [:the carrier of G,the carrier of G:] by FUNCT_2:def 1;
A5: rng x1 c= the carrier of G by FINSEQ_1:def 4;
rng x2 c= the carrier of G by FINSEQ_1:def 4;
then A8: [:(rng x1),(rng x2):] c= dom the multF of G by A5, A4, ZFMISC_1:119;
mlt x1,x2 = the multF of G .: x1,x2 by FVSUM_1:def 7;
then dom (mlt x1,x2) = (dom x1) /\ (dom x2) by A8, FUNCOP_1:84;
then A6: ( i in dom x1 & i in dom x2 ) by A1, XBOOLE_0:def 4;
then A2: x1 /. i = x1 . i by PARTFUN1:def 8;
A3: x2 /. i = x2 . i by A6, PARTFUN1:def 8;
thus (mlt x1,x2) . i = (x1 /. i) * (x2 /. i) by A1, A2, A3, FVSUM_1:73; :: thesis:
hence (mlt x1,x2) /. i = (x1 /. i) * (x2 /. i) by A1, PARTFUN1:def 8; :: thesis: