defpred S1[ object , object ] means ex f being Function of (F2() . $1),(F3() . $1) st
( $2 = f & ( for x being set st x in F2() . $1 holds
( f . x in F3() . $1 & P1[$1,x,f . x] ) ) );
A2:
for i being object st i in F1() holds
ex y being object st S1[i,y]
proof
let i be
object ;
( i in F1() implies ex y being object st S1[i,y] )
assume A3:
i in F1()
;
ex y being object st S1[i,y]
defpred S2[
object ,
object ]
means ( $2
in F3()
. i &
P1[
i,$1,$2] );
A4:
now for x being object st x in F2() . i holds
ex y being object st
( y in F3() . i & S2[x,y] )let x be
object ;
( x in F2() . i implies ex y being object st
( y in F3() . i & S2[x,y] ) )assume
x in F2()
. i
;
ex y being object st
( y in F3() . i & S2[x,y] )then
ex
y being
object st
(
y in F3()
. i &
P1[
i,
x,
y] )
by A1, A3;
hence
ex
y being
object st
(
y in F3()
. i &
S2[
x,
y] )
;
verum end;
consider f being
Function such that A5:
(
dom f = F2()
. i &
rng f c= F3()
. i )
and A6:
for
x being
object st
x in F2()
. i holds
S2[
x,
f . x]
from FUNCT_1:sch 6(A4);
reconsider f =
f as
Function of
(F2() . i),
(F3() . i) by A5, FUNCT_2:2;
take
f
;
S1[i,f]
take
f
;
( f = f & ( for x being set st x in F2() . i holds
( f . x in F3() . i & P1[i,x,f . x] ) ) )
thus
(
f = f & ( for
x being
set st
x in F2()
. i holds
(
f . x in F3()
. i &
P1[
i,
x,
f . x] ) ) )
by A6;
verum
end;
consider F being Function such that
A7:
dom F = F1()
and
A8:
for i being object st i in F1() holds
S1[i,F . i]
from CLASSES1:sch 1(A2);
reconsider F = F as ManySortedSet of F1() by A7, PARTFUN1:def 2, RELAT_1:def 18;
then reconsider F = F as ManySortedFunction of F2(),F3() by PBOOLE:def 15;
take
F
; for i, x being object st i in F1() & x in F2() . i holds
( (F . i) . x in F3() . i & P1[i,x,(F . i) . x] )
let i, x be object ; ( i in F1() & x in F2() . i implies ( (F . i) . x in F3() . i & P1[i,x,(F . i) . x] ) )
assume
i in F1()
; ( not x in F2() . i or ( (F . i) . x in F3() . i & P1[i,x,(F . i) . x] ) )
then
ex f being Function of (F2() . i),(F3() . i) st
( F . i = f & ( for x being set st x in F2() . i holds
( f . x in F3() . i & P1[i,x,f . x] ) ) )
by A8;
hence
( not x in F2() . i or ( (F . i) . x in F3() . i & P1[i,x,(F . i) . x] ) )
; verum