defpred S₁[ object , object ] means for X being set st X = $1 holds
$2 = SignGen (f,B,X);
A1: for x being object st x in F holds
ex y being object st
( y in D * & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in F implies ex y being object st
( y in D * & S₁[x,y] ) )
assume A2: x in F ; :: thesis: ex y being object st
( y in D * & S₁[x,y] )
reconsider X = x as set by A2;
take SignGen (f,B,X) ; :: thesis: ( SignGen (f,B,X) in D * & S₁[x, SignGen (f,B,X)] )
thus ( SignGen (f,B,X) in D * & S₁[x, SignGen (f,B,X)] ) by FINSEQ_1:def 11; :: thesis: verum

end;

consider f being Function of F,(D *) such that
A3: for x being object st x in F holds
S₁[x,f . x] from FUNCT_2:sch 1(A1);
take f ; :: thesis: for X being set st X in F holds
f . X = SignGen (f,B,X)
thus for X being set st X in F holds
f . X = SignGen (f,B,X) by A3; :: thesis: verum