defpred S1[ object , object ] means for y, z being object st $2 `1 = y & $2 `2 = z holds
P1[$1,y,z];
A2:
for x being object st x in F1() holds
ex p being object st
( p in [:F2(),F3():] & S1[x,p] )
proof
let x be
object ;
( x in F1() implies ex p being object st
( p in [:F2(),F3():] & S1[x,p] ) )
assume
x in F1()
;
ex p being object st
( p in [:F2(),F3():] & S1[x,p] )
then consider y,
z being
object such that A3:
(
y in F2() &
z in F3() )
and A4:
P1[
x,
y,
z]
by A1;
reconsider p =
[y,z] as
set ;
take
p
;
( p in [:F2(),F3():] & S1[x,p] )
thus
p in [:F2(),F3():]
by A3, ZFMISC_1:87;
S1[x,p]
thus
for
y,
z being
object st
p `1 = y &
p `2 = z holds
P1[
x,
y,
z]
by A4;
verum
end;
consider h being Function such that
( dom h = F1() & rng h c= [:F2(),F3():] )
and
A5:
for x being object st x in F1() holds
S1[x,h . x]
from FUNCT_1:sch 6(A2);
deffunc H1( object ) -> object = (h . $1) `2 ;
deffunc H2( object ) -> object = (h . $1) `1 ;
consider f being Function such that
A6:
dom f = F1()
and
A7:
for x being object st x in F1() holds
f . x = H2(x)
from FUNCT_1:sch 3();
consider g being Function such that
A8:
dom g = F1()
and
A9:
for x being object st x in F1() holds
g . x = H1(x)
from FUNCT_1:sch 3();
take
f
; ex g being Function st
( dom f = F1() & dom g = F1() & ( for x being object st x in F1() holds
P1[x,f . x,g . x] ) )
take
g
; ( dom f = F1() & dom g = F1() & ( for x being object st x in F1() holds
P1[x,f . x,g . x] ) )
thus
( dom f = F1() & dom g = F1() )
by A6, A8; for x being object st x in F1() holds
P1[x,f . x,g . x]
thus
for x being object st x in F1() holds
P1[x,f . x,g . x]
verumproof
let x be
object ;
( x in F1() implies P1[x,f . x,g . x] )
assume A10:
x in F1()
;
P1[x,f . x,g . x]
then
(
f . x = (h . x) `1 &
g . x = (h . x) `2 )
by A7, A9;
hence
P1[
x,
f . x,
g . x]
by A5, A10;
verum
end;