let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S

for X being V2() ManySortedSet of the carrier of S

for F being ManySortedFunction of X, the Sorts of A holds rngs F c= rngs (F -hash)

let A be non-empty MSAlgebra over S; :: thesis: for X being V2() ManySortedSet of the carrier of S

for F being ManySortedFunction of X, the Sorts of A holds rngs F c= rngs (F -hash)

let X be V2() ManySortedSet of the carrier of S; :: thesis: for F being ManySortedFunction of X, the Sorts of A holds rngs F c= rngs (F -hash)

let F be ManySortedFunction of X, the Sorts of A; :: thesis: rngs F c= rngs (F -hash)

set R = Reverse X;

let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in the carrier of S or (rngs F) . i c= (rngs (F -hash)) . i )

assume i in the carrier of S ; :: thesis: (rngs F) . i c= (rngs (F -hash)) . i

then reconsider s = i as SortSymbol of S ;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (rngs F) . i or y in (rngs (F -hash)) . i )

A1: dom ((Reverse X) . s) = (FreeGen X) . s by FUNCT_2:def 1;

FreeGen X c= the Sorts of (FreeMSA X) by PBOOLE:def 18;

then A2: (FreeGen X) . s c= the Sorts of (FreeMSA X) . s ;

assume y in (rngs F) . i ; :: thesis: y in (rngs (F -hash)) . i

then y in rng (F . s) by MSSUBFAM:13;

then consider x being object such that

A3: x in dom (F . s) and

A4: y = (F . s) . x by FUNCT_1:def 3;

rngs (Reverse X) = X by EXTENS_1:10;

then Reverse X is "onto" by EXTENS_1:9;

then rng ((Reverse X) . s) = X . s by MSUALG_3:def 3;

then consider a being object such that

A5: a in dom ((Reverse X) . s) and

A6: x = ((Reverse X) . s) . a by A3, FUNCT_1:def 3;

A7: dom ((F -hash) . s) = the Sorts of (FreeMSA X) . s by FUNCT_2:def 1;

y = ((F . s) * ((Reverse X) . s)) . a by A4, A5, A6, FUNCT_1:13

.= ((F ** (Reverse X)) . s) . a by MSUALG_3:2

.= (((F -hash) || (FreeGen X)) . s) . a by Def1

.= (((F -hash) . s) | ((FreeGen X) . s)) . a by MSAFREE:def 1

.= ((F -hash) . s) . a by A5, FUNCT_1:49 ;

then y in rng ((F -hash) . s) by A5, A1, A7, A2, FUNCT_1:def 3;

hence y in (rngs (F -hash)) . i by MSSUBFAM:13; :: thesis: verum

for X being V2() ManySortedSet of the carrier of S

for F being ManySortedFunction of X, the Sorts of A holds rngs F c= rngs (F -hash)

let A be non-empty MSAlgebra over S; :: thesis: for X being V2() ManySortedSet of the carrier of S

for F being ManySortedFunction of X, the Sorts of A holds rngs F c= rngs (F -hash)

let X be V2() ManySortedSet of the carrier of S; :: thesis: for F being ManySortedFunction of X, the Sorts of A holds rngs F c= rngs (F -hash)

let F be ManySortedFunction of X, the Sorts of A; :: thesis: rngs F c= rngs (F -hash)

set R = Reverse X;

let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in the carrier of S or (rngs F) . i c= (rngs (F -hash)) . i )

assume i in the carrier of S ; :: thesis: (rngs F) . i c= (rngs (F -hash)) . i

then reconsider s = i as SortSymbol of S ;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (rngs F) . i or y in (rngs (F -hash)) . i )

A1: dom ((Reverse X) . s) = (FreeGen X) . s by FUNCT_2:def 1;

FreeGen X c= the Sorts of (FreeMSA X) by PBOOLE:def 18;

then A2: (FreeGen X) . s c= the Sorts of (FreeMSA X) . s ;

assume y in (rngs F) . i ; :: thesis: y in (rngs (F -hash)) . i

then y in rng (F . s) by MSSUBFAM:13;

then consider x being object such that

A3: x in dom (F . s) and

A4: y = (F . s) . x by FUNCT_1:def 3;

rngs (Reverse X) = X by EXTENS_1:10;

then Reverse X is "onto" by EXTENS_1:9;

then rng ((Reverse X) . s) = X . s by MSUALG_3:def 3;

then consider a being object such that

A5: a in dom ((Reverse X) . s) and

A6: x = ((Reverse X) . s) . a by A3, FUNCT_1:def 3;

A7: dom ((F -hash) . s) = the Sorts of (FreeMSA X) . s by FUNCT_2:def 1;

y = ((F . s) * ((Reverse X) . s)) . a by A4, A5, A6, FUNCT_1:13

.= ((F ** (Reverse X)) . s) . a by MSUALG_3:2

.= (((F -hash) || (FreeGen X)) . s) . a by Def1

.= (((F -hash) . s) | ((FreeGen X) . s)) . a by MSAFREE:def 1

.= ((F -hash) . s) . a by A5, FUNCT_1:49 ;

then y in rng ((F -hash) . s) by A5, A1, A7, A2, FUNCT_1:def 3;

hence y in (rngs (F -hash)) . i by MSSUBFAM:13; :: thesis: verum