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 ()

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 ()

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 ()
let F be ManySortedFunction of X, the Sorts of A; :: thesis: rngs F c= rngs ()
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 ()) . i )
assume i in the carrier of S ; :: thesis: (rngs F) . i c= (rngs ()) . 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 ()) . i )
A1: dom (() . s) = () . s by FUNCT_2:def 1;
FreeGen X c= the Sorts of () by PBOOLE:def 18;
then A2: (FreeGen X) . s c= the Sorts of () . s ;
assume y in (rngs F) . i ; :: thesis: y in (rngs ()) . 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 () = X by EXTENS_1:10;
then Reverse X is "onto" by EXTENS_1:9;
then rng (() . s) = X . s by MSUALG_3:def 3;
then consider a being object such that
A5: a in dom (() . s) and
A6: x = (() . s) . a by ;
A7: dom (() . s) = the Sorts of () . s by FUNCT_2:def 1;
y = ((F . s) * (() . s)) . a by
.= ((F ** ()) . s) . a by MSUALG_3:2
.= ((() || ()) . s) . a by Def1
.= ((() . s) | (() . s)) . a by MSAFREE:def 1
.= (() . s) . a by ;
then y in rng (() . s) by ;
hence y in (rngs ()) . i by MSSUBFAM:13; :: thesis: verum