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 variables_in t) . s) by A1, PBOOLE:def 5;
hence V . s = (X . s) /\ { (a `1) where a is Element of rng t : a `2 = s } by A2, Def2; :: 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: V = X variables_in t

now :: thesis: for s being object st s in the carrier of S holds
V . s = (X . s) /\ ((S variables_in t) . s)

let s be object ; :: thesis: ( s in the carrier of S implies V . s = (X . s) /\ ((S variables_in t) . s) )
assume A4: s in the carrier of S ; :: thesis: V . s = (X . s) /\ ((S variables_in t) . s)
hence V . s = (X . s) /\ { (a `1) where a is Element of rng t : a `2 = s } by A3
.= (X . s) /\ ((S variables_in t) . s) by A4, Def2 ;
:: thesis: verum

end;

hence V = X variables_in t by PBOOLE:def 5; :: thesis: verum