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 product (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 product (MSFuncs A,B) )
assume A1:
A is_transformable_to B
; for g being ManySortedFunction of A,B holds g in product (MSFuncs A,B)
set f = MSFuncs A,B;
let g be ManySortedFunction of A,B; g in product (MSFuncs A,B)
A2:
dom (MSFuncs A,B) = I
by PARTFUN1:def 4;
A3:
now let x be
set ;
( x in dom (MSFuncs A,B) implies g . x in (MSFuncs A,B) . x )assume A4:
x in dom (MSFuncs A,B)
;
g . x in (MSFuncs A,B) . xthen reconsider i =
x as
Element of
I by PARTFUN1:def 4;
A5:
g . i is
Function of
(A . i),
(B . i)
by A2, A4, PBOOLE:def 18;
(
B . i = {} implies
A . i = {} )
by A1, A2, A4, PZFMISC1:def 3;
then
g . i in Funcs (A . i),
(B . i)
by A5, FUNCT_2:11;
hence
g . x in (MSFuncs A,B) . x
by A2, A4, PBOOLE:def 22;
verum end;
dom g = I
by PARTFUN1:def 4;
hence
g in product (MSFuncs A,B)
by A2, A3, CARD_3:18; verum