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

now

let i be set ; :: 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
A2: dom (Reverse X) = the carrier of S by PARTFUN1:def 4;
reconsider r = (Reverse X) . i as Function of ((FreeGen X) . i),(X . i) by A1, PBOOLE:def 18;
thus (rngs (Reverse X)) . i = X . i :: thesis: verum

proof

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 set ; :: 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:31;
rng r c= X . i by RELAT_1:def 19;
hence x in X . i by A3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X . i or x in (rngs (Reverse X)) . i )
assume A4: x in X . i ; :: thesis: x in (rngs (Reverse X)) . i
reconsider s0 = i as SortSymbol of S by A1;
set D = DTConMSA X;
A5: [x,s0] in Terminals (DTConMSA X) by A4, MSAFREE:7;
then reconsider t = [x,s0] as Symbol of (DTConMSA X) ;
A6: (Reverse X) . s0 = Reverse s0,X by MSAFREE:def 20;
then A7: dom ((Reverse X) . s0) = FreeGen s0,X by FUNCT_2:def 1;
t `2 = s0 by MCART_1:7;
then root-tree t in { (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s0 ) } by A5;
then A8: root-tree t in FreeGen s0,X by MSAFREE:14;
then A9: ((Reverse X) . s0) . (root-tree t) in rng ((Reverse X) . s0) by A7, FUNCT_1:def 5;
((Reverse X) . s0) . (root-tree t) = t `1 by A6, A8, MSAFREE:def 19
.= x by MCART_1:7 ;
hence x in (rngs (Reverse X)) . i by A2, A9, FUNCT_6:31; :: thesis: verum

end;

end;

hence rngs (Reverse X) = X by PBOOLE:3; :: thesis: verum