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 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:
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),() by ;
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