let i, j be Nat; :: thesis: for R1, R2 being Element of i -tuples_on COMPLEX holds (mlt (R1,R2)) . j = (R1 . j) * (R2 . j)
let R1, R2 be Element of i -tuples_on COMPLEX; :: thesis: (mlt (R1,R2)) . j = (R1 . j) * (R2 . j)
reconsider i = i, j1 = j as Element of NAT by ORDINAL1:def 12;
reconsider R1 = R1, R2 = R2 as Element of i -tuples_on COMPLEX ;

per cases ( not j in Seg i or j in Seg i ) ;

suppose A1: not j in Seg i ; :: thesis: (mlt (R1,R2)) . j = (R1 . j) * (R2 . j)

then A2: not j in dom R2 by FINSEQ_2:124;
not j in dom (mlt (R1,R2)) by A1, FINSEQ_2:124;
then (mlt (R1,R2)) . j = (R1 . j1) * 0 by FUNCT_1:def 2
.= (R1 . j) * (R2 . j) by A2, FUNCT_1:def 2 ;
hence (mlt (R1,R2)) . j = (R1 . j) * (R2 . j) ; :: thesis: verum

end;

suppose j in Seg i ; :: thesis: (mlt (R1,R2)) . j = (R1 . j) * (R2 . j)

then j in dom (mlt (R1,R2)) by FINSEQ_2:124;
hence (mlt (R1,R2)) . j = (R1 . j) * (R2 . j) by Th17; :: thesis: verum

end;

end;