set aK = addFinS K;
set KK = the carrier of K;
let p1, p2, p3 be Element of the carrier of K * ; BINOP_1:def 3 (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 for k being Nat st k in dom (p12 + p3) holds
(p1 + p23) . k = (p12 + p3) . klet k be
Nat;
( k in dom (p12 + p3) implies (p1 + p23) . k = (p12 + p3) . k )assume A11:
k in dom (p12 + p3)
;
(p1 + p23) . k = (p12 + p3) . kA12:
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;
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
; verum