let I be set ; 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; ( 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
; 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; g in MSFuncs (A,B)
A2:
dom ((Funcs) (A,B)) = I
by PARTFUN1:def 2;
A3:
now for x being object st x in dom ((Funcs) (A,B)) holds
g . x in ((Funcs) (A,B)) . xlet x be
object ;
( x in dom ((Funcs) (A,B)) implies g . x in ((Funcs) (A,B)) . x )assume A4:
x in dom ((Funcs) (A,B))
;
g . x in ((Funcs) (A,B)) . xthen 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;
verum end;
dom g = 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; verum