let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for B being non empty FinSequence of the carrier of S
for D being b₂ -sorts FinSequence of (Free (S,X))
for V being b₂ -sorts FinSequence of Union X st V is D -omitting holds
for b1, b2 being Element of dom B holds D . b1 is V . b2 -omitting
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for B being non empty FinSequence of the carrier of S
for D being b₁ -sorts FinSequence of (Free (S,X))
for V being b₁ -sorts FinSequence of Union X st V is D -omitting holds
for b1, b2 being Element of dom B holds D . b1 is V . b2 -omitting
let B be non empty FinSequence of the carrier of S; :: thesis: for D being B -sorts FinSequence of (Free (S,X))
for V being B -sorts FinSequence of Union X st V is D -omitting holds
for b1, b2 being Element of dom B holds D . b1 is V . b2 -omitting
let D be B -sorts FinSequence of (Free (S,X)); :: thesis: for V being B -sorts FinSequence of Union X st V is D -omitting holds
for b1, b2 being Element of dom B holds D . b1 is V . b2 -omitting
let V be B -sorts FinSequence of Union X; :: thesis: ( V is D -omitting implies for b1, b2 being Element of dom B holds D . b1 is V . b2 -omitting )
assume Z0: V is D -omitting ; :: thesis: for b1, b2 being Element of dom B holds D . b1 is V . b2 -omitting
let b1, b2 be Element of dom B; :: thesis: D . b1 is V . b2 -omitting
( dom D = dom B & dom V = dom B ) by SORTS, SORTS2;
then ( D . b1 in rng D & V . b2 in rng V ) by FUNCT_1:def 3;
then V . b2 nin vf (D . b1) by Z0, XBOOLE_0:3;
hence D . b1 is V . b2 -omitting by Th92; :: thesis: verum