let S be non empty non void ManySortedSign ; for o being OperSymbol of S
for X being V5() 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; for X being V5() 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 V5() 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 p be Element of Args (o,(Free (S,X))); 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 }
XBOOLE_0:def 10 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 ;
TARSKI:def 3 ( 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)
;
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;
verum
end;
let a be object ; TARSKI:def 3 ( 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 }
; 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; verum