let I be set ; :: thesis:
let A, B be ManySortedSet of I; :: thesis:
assume A1: A is_transformable_to B ; :: thesis:
set f = (Funcs) (A,B);
let x be set ; :: thesis:
assume x in MSFuncs (A,B) ; :: thesis:
then x in product ((Funcs) (A,B)) by A1, Def4;
then consider g being Function such that
A2: x = g and
A3: dom g = dom ((Funcs) (A,B)) and
A4: for i being object st i in dom ((Funcs) (A,B)) holds
g . i in ((Funcs) (A,B)) . i by CARD_3:def 5;
A5: dom ((Funcs) (A,B)) = I by PARTFUN1:def 2;
A6: for i being set st i in I holds
g . i in Funcs ((A . i),(B . i))

let i be set ; :: thesis:
assume A7: i in I ; :: thesis:
then ((Funcs) (A,B)) . i = Funcs ((A . i),(B . i)) by PBOOLE:def 17;
hence g . i in Funcs ((A . i),(B . i)) by A4, A5, A7; :: thesis:

end;

A8: for i being set st i in I holds
ex F being Function st
( F = g . i & dom F = A . i & rng F c= B . i )

let i be set ; :: thesis:
assume i in I ; :: thesis:
then g . i in Funcs ((A . i),(B . i)) by A6;
hence ex F being Function st
( F = g . i & dom F = A . i & rng F c= B . i ) by FUNCT_2:def 2; :: thesis:

end;

A9: for i being object st i in I holds
g . i is Function of (A . i),(B . i)

let i be object ; :: thesis:
assume A10: i in I ; :: thesis:
ex F being Function st
( F = g . i & dom F = A . i & rng F c= B . i ) by A8, A10;
hence g . i is Function of (A . i),(B . i) by FUNCT_2:2; :: thesis:

end;