defpred S1[ 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 S1[i,X]
proof
let i be object ; :: thesis: ( i in Seg d implies ex X being object st S1[i,X] )
assume i in Seg d ; :: thesis: ex X being object st S1[i,X]
set X = the non trivial finite Subset of REAL;
take the non trivial finite Subset of REAL ; :: thesis: S1[i, the non trivial finite Subset of REAL]
thus S1[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
S1[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