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