set KK = the carrier of K;
let p1, p2 be Element of the carrier of K * ; :: according to BINOP_1:def 13 :: thesis: (addFinS K) . p1,p2 = (addFinS K) . p2,p1
A1: ( rng p1 c= the carrier of K & rng p2 c= the carrier of K ) by FINSEQ_1:def 4;
A2: ( dom (p1 + p2) = (dom p1) /\ (dom p2) & dom (p2 + p1) = (dom p2) /\ (dom p1) ) by Lm9;

now

let k be Nat; :: thesis: ( k in dom (p1 + p2) implies (p1 + p2) . k = (p2 + p1) . k )
assume A3: k in dom (p1 + p2) ; :: thesis: (p1 + p2) . k = (p2 + p1) . k
( k in dom p1 & k in dom p2 ) by A2, A3, XBOOLE_0:def 4;
then ( p1 . k in rng p1 & p2 . k in rng p2 ) by FUNCT_1:def 5;
then reconsider p1k = p1 . k, p2k = p2 . k as Element of K by A1;
( (p1 + p2) . k = p1k + p2k & (p2 + p1) . k = p2k + p1k ) by A2, A3, FVSUM_1:21;
hence (p1 + p2) . k = (p2 + p1) . k ; :: thesis: verum

end;

then ( p1 + p2 = p2 + p1 & (addFinS K) . p1,p2 = p1 + p2 ) by A2, Def5, FINSEQ_1:17;
hence (addFinS K) . p1,p2 = (addFinS K) . p2,p1 by Def5; :: thesis: verum