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 ;
( B . i = {} implies A . i = {} ) by A1, A2, A4;
then g . i in Funcs ((A . i),(B . i)) by ;
hence g . x in ((Funcs) (A,B)) . x by ; :: thesis: verum
end;
dom g = I by PARTFUN1:def 2;
then g in product ((Funcs) (A,B)) by ;
hence g in MSFuncs (A,B) by ; :: thesis: verum