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