A2:
for x being set st x in F1() holds
ex y being set st P1[x,y]
proof
let x be
set ;
( x in F1() implies ex y being set st P1[x,y] )
assume A3:
x in F1()
;
ex y being set st P1[x,y]
reconsider p =
x as
Element of
F1()
by A3;
A4:
ex
y being
set st
P1[
p,
y]
by A1;
thus
ex
y being
set st
P1[
x,
y]
by A4;
verum
end;
consider f being Function such that
A5:
( dom f = F1() & ( for x being set st x in F1() holds
P1[x,f . x] ) )
from CLASSES1:sch 1(A2);
reconsider T = f as DecoratedTree by A5, Def8;
take
T
; ( dom T = F1() & ( for p being FinSequence of NAT st p in F1() holds
P1[p,T . p] ) )
thus
( dom T = F1() & ( for p being FinSequence of NAT st p in F1() holds
P1[p,T . p] ) )
by A5; verum