let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for X being V8() ManySortedSet of
for F being ManySortedFunction of X,the Sorts of A holds rngs F c= rngs (F -hash )
let A be non-empty MSAlgebra of S; :: thesis: for X being V8() ManySortedSet of
for F being ManySortedFunction of X,the Sorts of A holds rngs F c= rngs (F -hash )
let X be V8() ManySortedSet of ; :: 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 set ; :: according to PBOOLE:def 5 :: 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 set ; :: according to TARSKI:def 3 :: thesis: ( not y in (rngs F) . i or y in (rngs (F -hash )) . i )
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 set such that
A1: ( x in dom (F . s) & y = (F . s) . x ) by FUNCT_1:def 5;
rngs (Reverse X) = X by EXTENS_1:14;
then Reverse X is "onto" by EXTENS_1:13;
then rng ((Reverse X) . s) = X . s by MSUALG_3:def 3;
then consider a being set such that
A2: ( a in dom ((Reverse X) . s) & x = ((Reverse X) . s) . a ) by A1, FUNCT_1:def 5;
A3: dom ((Reverse X) . s) = (FreeGen X) . s by FUNCT_2:def 1;
A4: dom ((F -hash ) . s) = the Sorts of (FreeMSA X) . s by FUNCT_2:def 1;
FreeGen X c= the Sorts of (FreeMSA X) by PBOOLE:def 23;
then A5: (FreeGen X) . s c= the Sorts of (FreeMSA X) . s by PBOOLE:def 5;
y = ((F . s) * ((Reverse X) . s)) . a by A1, A2, FUNCT_1:23
.= ((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 A2, FUNCT_1:72 ;
then y in rng ((F -hash ) . s) by A2, A3, A4, A5, FUNCT_1:def 5;
hence y in (rngs (F -hash )) . i by MSSUBFAM:13; :: thesis: verum