set aK = addFinS K;
set KK = the carrier of K;
let p1, p2, p3 be Element of the carrier of K * ; :: according to BINOP_1:def 3 :: thesis: (addFinS K) . (p1,((addFinS K) . (p2,p3))) = (addFinS K) . (((addFinS K) . (p1,p2)),p3)
reconsider p12 = p1 + p2, p23 = p2 + p3 as Element of the carrier of K * by FINSEQ_1:def 11;
A1: rng p1 c= the carrier of K by FINSEQ_1:def 4;
A2: rng p2 c= the carrier of K by FINSEQ_1:def 4;
A3: rng p12 c= the carrier of K by FINSEQ_1:def 4;
A4: rng p3 c= the carrier of K by FINSEQ_1:def 4;
A5: rng p23 c= the carrier of K by FINSEQ_1:def 4;
A6: dom p12 = (dom p1) /\ (dom p2) by Lm9;
A7: dom p23 = (dom p2) /\ (dom p3) by Lm9;
A8: dom (p12 + p3) = (dom p12) /\ (dom p3) by Lm9;
A9: dom (p1 + p23) = (dom p1) /\ (dom p23) by Lm9;
then A10: dom (p12 + p3) = dom (p1 + p23) by A6, A8, A7, XBOOLE_1:16;

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

let k be Nat; :: thesis: ( k in dom (p12 + p3) implies (p1 + p23) . k = (p12 + p3) . k )
assume A11: k in dom (p12 + p3) ; :: thesis: (p1 + p23) . k = (p12 + p3) . k
A12: k in dom p12 by A8, A11, XBOOLE_0:def 4;
then A13: p12 . k in rng p12 by FUNCT_1:def 3;
k in dom p1 by A6, A12, XBOOLE_0:def 4;
then A14: p1 . k in rng p1 by FUNCT_1:def 3;
A15: k in dom p3 by A8, A11, XBOOLE_0:def 4;
then A16: p3 . k in rng p3 by FUNCT_1:def 3;
A17: k in dom p2 by A6, A12, XBOOLE_0:def 4;
then A18: p2 . k in rng p2 by FUNCT_1:def 3;
A19: k in dom p23 by A7, A15, A17, XBOOLE_0:def 4;
then p23 . k in rng p23 by FUNCT_1:def 3;
then reconsider p1k = p1 . k, p12k = p12 . k, p2k = p2 . k, p23k = p23 . k, p3k = p3 . k as Element of K by A1, A2, A4, A3, A5, A14, A13, A16, A18;
A20: p12 . k = p1k + p2k by A12, FVSUM_1:17;
A21: (p12 + p3) . k = p12k + p3k by A11, FVSUM_1:17;
A22: p23 . k = p2k + p3k by A19, FVSUM_1:17;
(p1 + p23) . k = p1k + p23k by A10, A11, FVSUM_1:17;
hence (p1 + p23) . k = (p12 + p3) . k by A20, A22, A21, RLVECT_1:def 3; :: thesis: verum

end;

then A23: p1 + p23 = p12 + p3 by A6, A8, A7, A9, FINSEQ_1:13, XBOOLE_1:16;
thus (addFinS K) . (p1,((addFinS K) . (p2,p3))) = (addFinS K) . (p1,p23) by Def5
.= p1 + p23 by Def5
.= (addFinS K) . (p12,p3) by A23, Def5
.= (addFinS K) . (((addFinS K) . (p1,p2)),p3) by Def5 ; :: thesis: verum