let S be ManySortedSign ; :: thesis: for X being ManySortedSet of the carrier of S
for t being non empty Relation
for V being ManySortedSubset of X holds
( V = X variables_in t iff for s being set st s in the carrier of S holds
V . s = (X . s) /\ { (a `1) where a is Element of rng t : a `2 = s } )

let X be ManySortedSet of the carrier of S; :: thesis: for t being non empty Relation
for V being ManySortedSubset of X holds
( V = X variables_in t iff for s being set st s in the carrier of S holds
V . s = (X . s) /\ { (a `1) where a is Element of rng t : a `2 = s } )

let t be non empty Relation; :: thesis: for V being ManySortedSubset of X holds
( V = X variables_in t iff for s being set st s in the carrier of S holds
V . s = (X . s) /\ { (a `1) where a is Element of rng t : a `2 = s } )

let V be ManySortedSubset of X; :: thesis: ( V = X variables_in t iff for s being set st s in the carrier of S holds
V . s = (X . s) /\ { (a `1) where a is Element of rng t : a `2 = s } )

hereby :: thesis: ( ( for s being set st s in the carrier of S holds
V . s = (X . s) /\ { (a `1) where a is Element of rng t : a `2 = s } ) implies V = X variables_in t )
assume A1: V = X variables_in t ; :: thesis: for s being set st s in the carrier of S holds
V . s = (X . s) /\ { (a `1) where a is Element of rng t : a `2 = s }

let s be set ; :: thesis: ( s in the carrier of S implies V . s = (X . s) /\ { (a `1) where a is Element of rng t : a `2 = s } )
assume A2: s in the carrier of S ; :: thesis: V . s = (X . s) /\ { (a `1) where a is Element of rng t : a `2 = s }
then V . s = (X . s) /\ (() . s) by ;
hence V . s = (X . s) /\ { (a `1) where a is Element of rng t : a `2 = s } by ; :: thesis: verum
end;
assume A3: for s being set st s in the carrier of S holds
V . s = (X . s) /\ { (a `1) where a is Element of rng t : a `2 = s } ; :: thesis:
now :: thesis: for s being object st s in the carrier of S holds
V . s = (X . s) /\ (() . s)
let s be object ; :: thesis: ( s in the carrier of S implies V . s = (X . s) /\ (() . s) )
assume A4: s in the carrier of S ; :: thesis: V . s = (X . s) /\ (() . s)
hence V . s = (X . s) /\ { (a `1) where a is Element of rng t : a `2 = s } by A3
.= (X . s) /\ (() . s) by ;
:: thesis: verum
end;
hence V = X variables_in t by PBOOLE:def 5; :: thesis: verum