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 2;
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 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, PZFMISC1:def 3;
then
g . i in Funcs (
(A . i),
(B . i))
by A5, FUNCT_2:8;
hence
g . x in (MSFuncs (A,B)) . x
by A2, A4, PBOOLE:def 17;
verum end;
dom g = I
by PARTFUN1:def 2;
hence
g in product (MSFuncs (A,B))
by A2, A3, CARD_3:9; verum