defpred S_{1}[ object , object ] means $2 is non trivial finite Subset of REAL;

A1: for i being object st i in Seg d holds

ex X being object st S_{1}[i,X]

A2: ( dom G = Seg d & ( for i being object st i in Seg d holds

S_{1}[i,G . i] ) )
from CLASSES1:sch 1(A1);

for i being object st i in Seg d holds

G . i in bool REAL

take G ; :: thesis: for i being Element of Seg d holds

( not G . i is trivial & G . i is finite )

thus for i being Element of Seg d holds

( not G . i is trivial & G . i is finite ) by A2; :: thesis: verum

A1: for i being object st i in Seg d holds

ex X being object st S

proof

consider G being Function such that
let i be object ; :: thesis: ( i in Seg d implies ex X being object st S_{1}[i,X] )

assume i in Seg d ; :: thesis: ex X being object st S_{1}[i,X]

set X = the non trivial finite Subset of REAL;

take the non trivial finite Subset of REAL ; :: thesis: S_{1}[i, the non trivial finite Subset of REAL]

thus S_{1}[i, the non trivial finite Subset of REAL]
; :: thesis: verum

end;assume i in Seg d ; :: thesis: ex X being object st S

set X = the non trivial finite Subset of REAL;

take the non trivial finite Subset of REAL ; :: thesis: S

thus S

A2: ( dom G = Seg d & ( for i being object st i in Seg d holds

S

for i being object st i in Seg d holds

G . i in bool REAL

proof

then reconsider G = G as Function of (Seg d),(bool REAL) by A2, FUNCT_2:3;
let i be object ; :: thesis: ( i in Seg d implies G . i in bool REAL )

assume i in Seg d ; :: thesis: G . i in bool REAL

then G . i is Subset of REAL by A2;

hence G . i in bool REAL ; :: thesis: verum

end;assume i in Seg d ; :: thesis: G . i in bool REAL

then G . i is Subset of REAL by A2;

hence G . i in bool REAL ; :: thesis: verum

take G ; :: thesis: for i being Element of Seg d holds

( not G . i is trivial & G . i is finite )

thus for i being Element of Seg d holds

( not G . i is trivial & G . i is finite ) by A2; :: thesis: verum