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

now :: thesis: for k being Nat st k in dom (p1 + p2) holds
(p1 + p2) . k = (p2 + p1) . k

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

end;

then A7: p1 + p2 = p2 + p1 by A3, Lm9, FINSEQ_1:13;
(addFinS K) . (p1,p2) = p1 + p2 by Def5;
hence (addFinS K) . (p1,p2) = (addFinS K) . (p2,p1) by A7, Def5; :: thesis: verum