let S be non empty non void ManySortedSign ; for A being non-empty MSAlgebra over S
for X being non-empty 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; for X being non-empty 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 non-empty ManySortedSet of the carrier of S; 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; rngs F c= rngs (F -hash)
set R = Reverse X;
let i be object ; PBOOLE:def 2 ( not i in the carrier of S or (rngs F) . i c= (rngs (F -hash)) . i )
assume
i in the carrier of S
; (rngs F) . i c= (rngs (F -hash)) . i
then reconsider s = i as SortSymbol of S ;
let y be object ; TARSKI:def 3 ( 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
; 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; verum