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;

then g in product ((Funcs) (A,B)) by A2, A3, CARD_3:9;

hence g in MSFuncs (A,B) by A1, Def4; :: thesis: verum

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

dom g = I
by PARTFUN1:def 2;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;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

then g in product ((Funcs) (A,B)) by A2, A3, CARD_3:9;

hence g in MSFuncs (A,B) by A1, Def4; :: thesis: verum