let I be set ; :: thesis: for A, B being ManySortedSet of I st A is_transformable_to B holds
for g being ManySortedFunction of A,B holds g in MSFuncs (A,B)
let A, B be ManySortedSet of I; :: thesis: ( A is_transformable_to B implies for g being ManySortedFunction of A,B holds g in MSFuncs (A,B) )
assume A1: A is_transformable_to B ; :: thesis: for g being ManySortedFunction of A,B holds g in MSFuncs (A,B)
set f = (Funcs) (A,B);
let g be ManySortedFunction of A,B; :: thesis: g in MSFuncs (A,B)
A2: dom ((Funcs) (A,B)) = I by PARTFUN1:def 2;

A3: now :: thesis: for x being object st x in dom ((Funcs) (A,B)) holds
g . x in ((Funcs) (A,B)) . x

let x be object ; :: thesis: ( x in dom ((Funcs) (A,B)) implies g . x in ((Funcs) (A,B)) . x )
assume A4: x in dom ((Funcs) (A,B)) ; :: thesis: g . x in ((Funcs) (A,B)) . x
then reconsider i = x as Element of I by PARTFUN1:def 2;
A5: g . i is Function of (A . i),(B . i) by A2, A4, PBOOLE:def 15;
( B . i = {} implies A . i = {} ) by A1, A2, A4;
then g . i in Funcs ((A . i),(B . i)) by A5, FUNCT_2:8;
hence g . x in ((Funcs) (A,B)) . x by A2, A4, PBOOLE:def 17; :: thesis: verum

end;

dom g = I by PARTFUN1:def 2;
then g in product ((Funcs) (A,B)) by A2, A3, CARD_3:9;
hence g in MSFuncs (A,B) by A1, Def4; :: thesis: verum