let I be set ; :: thesis: for A, B being ManySortedSet of
for F being ManySortedFunction of st A is_transformable_to B & F is ManySortedFunction of A,B holds
( doms F = A & rngs F c= B )
let A, B be ManySortedSet of ; :: thesis: for F being ManySortedFunction of st A is_transformable_to B & F is ManySortedFunction of A,B holds
( doms F = A & rngs F c= B )
let F be ManySortedFunction of ; :: thesis: ( A is_transformable_to B & F is ManySortedFunction of A,B implies ( doms F = A & rngs F c= B ) )
assume that
A1: A is_transformable_to B and
A2: F is ManySortedFunction of A,B ; :: thesis: ( doms F = A & rngs F c= B )

now

let i be set ; :: thesis: ( i in I implies (doms F) . i = A . i )
assume A3: i in I ; :: thesis: (doms F) . i = A . i
then reconsider f = F . i as Function of (A . i),(B . i) by A2, PBOOLE:def 18;
A4: ( B . i = {} implies A . i = {} ) by A1, A3, PZFMISC1:def 3;
thus (doms F) . i = dom f by A3, Th14
.= A . i by A4, FUNCT_2:def 1 ; :: thesis: verum

end;

hence doms F = A by PBOOLE:3; :: thesis: rngs F c= B
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or (rngs F) . i c= B . i )
assume A5: i in I ; :: thesis: (rngs F) . i c= B . i
then reconsider f = F . i as Function of (A . i),(B . i) by A2, PBOOLE:def 18;
rng f c= B . i by RELAT_1:def 19;
hence (rngs F) . i c= B . i by A5, Th13; :: thesis: verum