let K be non empty addLoopStr ; for p1, p2 being FinSequence of the carrier of K st dom p1 = dom p2 holds
dom (p1 + p2) = dom p1
let p1, p2 be FinSequence of the carrier of K; ( dom p1 = dom p2 implies dom (p1 + p2) = dom p1 )
assume A1:
dom p1 = dom p2
; dom (p1 + p2) = dom p1
A2:
( rng <:p1,p2:> c= [:(rng p1),(rng p2):] & [:(rng p1),(rng p2):] c= [: the carrier of K, the carrier of K:] )
by FUNCT_3:51, ZFMISC_1:96;
A3:
[: the carrier of K, the carrier of K:] = dom the addF of K
by FUNCT_2:def 1;
thus dom (p1 + p2) =
dom ( the addF of K .: (p1,p2))
by FVSUM_1:def 3
.=
dom <:p1,p2:>
by A2, A3, RELAT_1:27, XBOOLE_1:1
.=
(dom p1) /\ (dom p2)
by FUNCT_3:def 7
.=
dom p1
by A1
; verum