let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for X being non-empty ManySortedSet of the carrier of S
for p being Element of Args (o,(Free (S,X))) holds vf (o -term p) = union { (vf t) where t is Element of (Free (S,X)) : t in rng p }
let o be OperSymbol of S; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for p being Element of Args (o,(Free (S,X))) holds vf (o -term p) = union { (vf t) where t is Element of (Free (S,X)) : t in rng p }
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for p being Element of Args (o,(Free (S,X))) holds vf (o -term p) = union { (vf t) where t is Element of (Free (S,X)) : t in rng p }
let p be Element of Args (o,(Free (S,X))); :: thesis: vf (o -term p) = union { (vf t) where t is Element of (Free (S,X)) : t in rng p }
B1: dom (X variables_in (o -term p)) = the carrier of S by PARTFUN1:def 2;
thus vf (o -term p) c= union { (vf t) where t is Element of (Free (S,X)) : t in rng p } :: according to XBOOLE_0:def 10 :: thesis: union { (vf t) where t is Element of (Free (S,X)) : t in rng p } c= vf (o -term p)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in vf (o -term p) or a in union { (vf t) where t is Element of (Free (S,X)) : t in rng p } )
assume a in vf (o -term p) ; :: thesis: a in union { (vf t) where t is Element of (Free (S,X)) : t in rng p }
then a in Union (X variables_in (o -term p)) by ThR1;
then consider b being object such that
A1: ( b in dom (X variables_in (o -term p)) & a in (X variables_in (o -term p)) . b ) by CARD_5:2;
reconsider b = b as SortSymbol of S by A1;
consider t being DecoratedTree such that
A2: ( t in rng p & a in (X variables_in t) . b ) by A1, MSAFREE3:13;
reconsider t = t as Element of (Free (S,X)) by A2, RELAT_1:167;
A3: dom (X variables_in t) = the carrier of S by PARTFUN1:def 2;
( a in Union (X variables_in t) & Union (X variables_in t) = vf t & vf t in { (vf t1) where t1 is Element of (Free (S,X)) : t1 in rng p } ) by A2, A3, ThR1, CARD_5:2;
hence a in union { (vf t1) where t1 is Element of (Free (S,X)) : t1 in rng p } by TARSKI:def 4; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union { (vf t) where t is Element of (Free (S,X)) : t in rng p } or a in vf (o -term p) )
assume a in union { (vf t) where t is Element of (Free (S,X)) : t in rng p } ; :: thesis: a in vf (o -term p)
then consider I being set such that
A4: ( a in I & I in { (vf t) where t is Element of (Free (S,X)) : t in rng p } ) by TARSKI:def 4;
consider t being Element of (Free (S,X)) such that
A5: ( I = vf t & t in rng p ) by A4;
a in Union (X variables_in t) by A4, A5, ThR1;
then consider b being object such that
A6: ( b in dom (X variables_in t) & a in (X variables_in t) . b ) by CARD_5:2;
reconsider b = b as SortSymbol of S by A6;
a in (X variables_in (o -term p)) . b by A5, A6, MSAFREE3:13;
then a in Union (X variables_in (o -term p)) by B1, CARD_5:2;
hence a in vf (o -term p) by ThR1; :: thesis: verum