defpred S₁[ 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₁[i,X]

proof

let i be object ; :: thesis: ( i in Seg d implies ex X being object st S₁[i,X] )
assume i in Seg d ; :: thesis: ex X being object st S₁[i,X]
set X = the non trivial finite Subset of REAL;
take the non trivial finite Subset of REAL ; :: thesis: S₁[i, the non trivial finite Subset of REAL]
thus S₁[i, the non trivial finite Subset of REAL] ; :: thesis: verum

end;

consider G being Function such that
A2: ( dom G = Seg d & ( for i being object st i in Seg d holds
S₁[i,G . i] ) ) from CLASSES1:sch 1(A1);
for i being object st i in Seg d holds
G . i in bool REAL

proof

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;

then reconsider G = G as Function of (Seg d),(bool REAL) by A2, FUNCT_2:3;
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