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:71, ZFMISC_1:119;
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 (the addF of K * <:p1,p2:>)
.=
dom <:p1,p2:>
by A2, A3, RELAT_1:46, XBOOLE_1:1
.=
(dom p1) /\ (dom p2)
by FUNCT_3:def 8
.=
dom p1
by A1
; verum