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)
A1: rng p2 c= the carrier of K by FINSEQ_1:def 4;
rng p1 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 A1, ZFMISC_1:96;
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:69; :: thesis: verum