let K be non empty addLoopStr ; :: thesis: for p1, p2 being Element of the carrier of K * holds dom (p1 + p2) = (dom p1) /\ (dom p2)
let p1, p2 be Element of the carrier of K * ; :: thesis: dom (p1 + p2) = (dom p1) /\ (dom p2)
( rng p1 c= the carrier of K & rng p2 c= the carrier of K ) by FINSEQ_1:def 4;
then [:(rng p1),(rng p2):] c= [:the carrier of K,the carrier of K:] by ZFMISC_1:119;
then [:(rng p1),(rng p2):] c= dom the addF of K by FUNCT_2:def 1;
hence dom (p1 + p2) = (dom p1) /\ (dom p2) by FUNCOP_1:84; :: thesis: verum