let S be ManySortedSign ; :: thesis: for X being ManySortedSet of
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 ; :: 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 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) & (S variables_in t) . s = { (a `1 ) where a is Element of rng t : a `2 = s } ) by A1, Def3, PBOOLE:def 8;
hence V . s = (X . s) /\ { (a `1 ) where a is Element of rng t : a `2 = s } ; :: thesis: verum

end;

assume A2: 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

let s be set ; :: thesis: ( s in the carrier of S implies V . s = (X . s) /\ ((S variables_in t) . s) )
assume A3: 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 A2
.= (X . s) /\ ((S variables_in t) . s) by A3, Def3 ;
:: thesis: verum

end;

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