theorem :: FOMODEL0:77

for b1, b2 being set
for f1, f2 being Function st (rng f1) /\ (rng f2) = {} & b1 <> b2 & rng f1 c= dom f2 & rng f2 c= dom f1 holds
[:(rng f1),{b2}:] \/ [:(rng f2),{b1}:] c= ((f1 \/ f2) >*> ([:(rng f1),{b2}:] \/ [:(rng f2),{b1}:])) >*> ((b1,b2) --> (b2,b1)) by Lm68;