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 } )

V . s = (X . s) /\ { (a `1) where a is Element of rng t : a `2 = s } ; :: thesis: V = X variables_in t

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 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 } ) 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;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

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)

hence
V = X variables_in t
by PBOOLE:def 5; :: thesis: verumV . 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;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