let S be non empty non void ManySortedSign ; for X being non-empty ManySortedSet of the carrier of S
for T being b1,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for r being Element of T holds vf r = Union (X variables_in r)
let X be non-empty ManySortedSet of the carrier of S; for T being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for r being Element of T holds vf r = Union (X variables_in r)
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; for r being Element of T holds vf r = Union (X variables_in r)
let r be Element of T; vf r = Union (X variables_in r)
thus
vf r c= Union (X variables_in r)
XBOOLE_0:def 10 Union (X variables_in r) c= vf rproof
let a be
object ;
TARSKI:def 3 ( not a in vf r or a in Union (X variables_in r) )
assume
a in vf r
;
a in Union (X variables_in r)
then consider b being
object such that A1:
[a,b] in (rng r) /\ [:(Union X), the carrier of S:]
by XTUPLE_0:def 12;
A2:
(
[a,b] in rng r &
[a,b] in [:(Union X), the carrier of S:] )
by A1, XBOOLE_0:def 4;
then
(
a in Union X &
b in the
carrier of
S )
by ZFMISC_1:87;
then consider c being
object such that A4:
(
c in dom X &
a in X . c )
by CARD_5:2;
reconsider b =
b,
c =
c as
SortSymbol of
S by A4, A2, ZFMISC_1:87;
consider d being
object such that A5:
(
d in dom r &
[a,b] = r . d )
by A2, FUNCT_1:def 3;
reconsider d =
d as
Element of
dom r by A5;
reconsider t =
r | d as
Element of
T by MSAFREE4:44;
A7:
(X variables_in r) . b = (X . b) /\ { (a `1) where a is Element of rng r : a `2 = b }
by MSAFREE3:9;
t is
Element of
(Free (S,X))
by MSAFREE4:39;
end;
let a be object ; TARSKI:def 3 ( not a in Union (X variables_in r) or a in vf r )
assume
a in Union (X variables_in r)
; a in vf r
then consider b being object such that
B1:
( b in dom (X variables_in r) & a in (X variables_in r) . b )
by CARD_5:2;
reconsider b = b as SortSymbol of S by B1;
(X variables_in r) . b = (X . b) /\ { (a `1) where a is Element of rng r : a `2 = b }
by MSAFREE3:9;
then B2:
( a in X . b & a in { (a `1) where a is Element of rng r : a `2 = b } )
by B1, XBOOLE_0:def 4;
then consider q being Element of rng r such that
B3:
( a = q `1 & q `2 = b )
;
dom X = the carrier of S
by PARTFUN1:def 2;
then
a in Union X
by B2, CARD_5:2;
then B6:
[a,b] in [:(Union X), the carrier of S:]
by ZFMISC_1:87;
consider xi being object such that
B4:
( xi in dom r & q = r . xi )
by FUNCT_1:def 3;
reconsider xi = xi as Element of dom r by B4;
reconsider t = r | xi as Element of T by MSAFREE4:44;
t is Element of (Free (S,X))
by MSAFREE4:39;