let K be commutative Ring; :: thesis: for pK, qK being FinSequence of K st len pK = len qK holds
len pK = len (pK + qK)
let pK, qK be FinSequence of K; :: thesis: ( len pK = len qK implies len pK = len (pK + qK) )
assume len pK = len qK ; :: thesis: len pK = len (pK + qK)
then A1: qK is Element of (len pK) -tuples_on the carrier of K by FINSEQ_2:92;
pK is Element of (len pK) -tuples_on the carrier of K by FINSEQ_2:92;
then pK + qK is Element of (len pK) -tuples_on the carrier of K by A1, FINSEQ_2:120;
hence len pK = len (pK + qK) by CARD_1:def 7; :: thesis: verum