let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of the carrier of S holds rngs (Reverse X) = X
let X be non-empty ManySortedSet of the carrier of S; :: thesis: rngs (Reverse X) = X
set I = the carrier of S;
set R = Reverse X;

now :: thesis: for i being object st i in the carrier of S holds
(rngs (Reverse X)) . i = X . i

let i be object ; :: thesis: ( i in the carrier of S implies (rngs (Reverse X)) . i = X . i )
assume A1: i in the carrier of S ; :: thesis: (rngs (Reverse X)) . i = X . i
reconsider r = (Reverse X) . i as Function of ((FreeGen X) . i),(X . i) by A1, PBOOLE:def 15;
A2: dom (Reverse X) = the carrier of S by PARTFUN1:def 2;
thus (rngs (Reverse X)) . i = X . i :: thesis: verum

proof

reconsider s0 = i as SortSymbol of S by A1;
set D = DTConMSA X;
thus (rngs (Reverse X)) . i c= X . i :: according to XBOOLE_0:def 10 :: thesis: X . i c= (rngs (Reverse X)) . i

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (rngs (Reverse X)) . i or x in X . i )
assume x in (rngs (Reverse X)) . i ; :: thesis: x in X . i
then A3: x in rng r by A1, A2, FUNCT_6:22;
rng r c= X . i by RELAT_1:def 19;
hence x in X . i by A3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X . i or x in (rngs (Reverse X)) . i )
assume x in X . i ; :: thesis: x in (rngs (Reverse X)) . i
then A4: [x,s0] in Terminals (DTConMSA X) by MSAFREE:7;
then reconsider t = [x,s0] as Symbol of (DTConMSA X) ;
t `2 = s0 ;
then root-tree t in { (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s0 ) } by A4;
then A5: root-tree t in FreeGen (s0,X) by MSAFREE:13;
A6: (Reverse X) . s0 = Reverse (s0,X) by MSAFREE:def 18;
then A7: ((Reverse X) . s0) . (root-tree t) = t `1 by A5, MSAFREE:def 17
.= x ;
dom ((Reverse X) . s0) = FreeGen (s0,X) by A6, FUNCT_2:def 1;
then ((Reverse X) . s0) . (root-tree t) in rng ((Reverse X) . s0) by A5, FUNCT_1:def 3;
hence x in (rngs (Reverse X)) . i by A2, A7, FUNCT_6:22; :: thesis: verum

end;

end;

hence rngs (Reverse X) = X ; :: thesis: verum