let I be set ; :: thesis: for A, B being ManySortedSet of I st A is_transformable_to B holds

for x being set st x in MSFuncs (A,B) holds

x is ManySortedFunction of A,B

let A, B be ManySortedSet of I; :: thesis: ( A is_transformable_to B implies for x being set st x in 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 MSFuncs (A,B) holds

x is ManySortedFunction of A,B

set f = (Funcs) (A,B);

let x be set ; :: thesis: ( x in MSFuncs (A,B) implies x is ManySortedFunction of A,B )

assume x in MSFuncs (A,B) ; :: thesis: x is ManySortedFunction of A,B

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

ex F being Function st

( F = g . i & dom F = A . i & rng F c= B . i )

g . i is Function of (A . i),(B . i)

then g is ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

hence x is ManySortedFunction of A,B by A2, A9, PBOOLE:def 15; :: thesis: verum

for x being set st x in MSFuncs (A,B) holds

x is ManySortedFunction of A,B

let A, B be ManySortedSet of I; :: thesis: ( A is_transformable_to B implies for x being set st x in 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 MSFuncs (A,B) holds

x is ManySortedFunction of A,B

set f = (Funcs) (A,B);

let x be set ; :: thesis: ( x in MSFuncs (A,B) implies x is ManySortedFunction of A,B )

assume x in MSFuncs (A,B) ; :: thesis: x is ManySortedFunction of A,B

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

proof

A8:
for i being set st i in I holds
let i be set ; :: thesis: ( i in I implies g . i in Funcs ((A . i),(B . i)) )

assume A7: i in I ; :: thesis: g . i in Funcs ((A . i),(B . i))

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: verum

end;assume A7: i in I ; :: thesis: g . i in Funcs ((A . i),(B . i))

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: verum

ex F being Function st

( F = g . i & dom F = A . i & rng F c= B . i )

proof

A9:
for i being object st i in I holds
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 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: verum

end;( 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 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: verum

g . i is Function of (A . i),(B . i)

proof

dom g = I
by A3, PARTFUN1:def 2;
let i be object ; :: thesis: ( i in I implies g . i is Function of (A . i),(B . i) )

assume A10: i in I ; :: thesis: g . i is Function of (A . i),(B . i)

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: verum

end;assume A10: i in I ; :: thesis: g . i is Function of (A . i),(B . i)

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: verum

then g is ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

hence x is ManySortedFunction of A,B by A2, A9, PBOOLE:def 15; :: thesis: verum