let I be set ; :: thesis: for A, B being ManySortedSet of I
for F being ManySortedFunction of I 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 I; :: thesis: for F being ManySortedFunction of I 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 I; :: 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 :: thesis: for i being object st i in I holds
(doms F) . i = A . i

let i be object ; :: 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 15;
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 ; :: thesis: rngs F c= B
let i be object ; :: according to PBOOLE:def 2 :: 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 15;
rng f c= B . i by RELAT_1:def 19;
hence (rngs F) . i c= B . i by A5, Th13; :: thesis: verum