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

proof

let i be set ; :: thesis: ( i in I implies g . i in Funcs (A . i),(B . i) )
assume A6: i in I ; :: thesis: g . i in Funcs (A . i),(B . i)
then (MSFuncs A,B) . i = Funcs (A . i),(B . i) by PBOOLE:def 22;
hence g . i in Funcs (A . i),(B . i) by A3, A4, A6; :: thesis: verum

end;

A7: 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 )

proof

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

end;

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

proof

let i be set ; :: thesis: ( i in I implies g . i is Function of (A . i),(B . i) )
assume A9: i in I ; :: thesis: g . i is Function of (A . i),(B . i)
then consider F being Function such that
A10: ( F = g . i & dom F = A . i & rng F c= B . i ) by A7;
( B . i = {} implies A . i = {} ) by A1, A9, PZFMISC1:def 3;
hence g . i is Function of (A . i),(B . i) by A10, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum

end;

dom g = I by A4;
then g is ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18;
hence x is ManySortedFunction of A,B by A3, A8, PBOOLE:def 18; :: thesis: verum