let i, j be Nat; :: thesis: for K being non empty multMagma
for a1, a2 being Element of K
for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds
(mlt (R1,R2)) . j = a1 * a2
let K be non empty multMagma ; :: thesis: for a1, a2 being Element of K
for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds
(mlt (R1,R2)) . j = a1 * a2
let a1, a2 be Element of K; :: thesis: for R1, R2 being Element of i -tuples_on the carrier of K st j in Seg i & a1 = R1 . j & a2 = R2 . j holds
(mlt (R1,R2)) . j = a1 * a2
let R1, R2 be Element of i -tuples_on the carrier of K; :: thesis: ( j in Seg i & a1 = R1 . j & a2 = R2 . j implies (mlt (R1,R2)) . j = a1 * a2 )
assume j in Seg i ; :: thesis: ( not a1 = R1 . j or not a2 = R2 . j or (mlt (R1,R2)) . j = a1 * a2 )
then j in Seg (len (mlt (R1,R2))) by CARD_1:def 7;
then j in dom (mlt (R1,R2)) by FINSEQ_1:def 3;
hence ( not a1 = R1 . j or not a2 = R2 . j or (mlt (R1,R2)) . j = a1 * a2 ) by FUNCOP_1:22; :: thesis: verum