let IT1, IT2 be Function of F,(D *); :: thesis: ( ( for X being set st X in F holds
IT1 . X = SignGen (f,B,X) ) & ( for X being set st X in F holds
IT2 . X = SignGen (f,B,X) ) implies IT1 = IT2 )
assume that
A4: for X being set st X in F holds
IT1 . X = SignGen (f,B,X) and
A5: for X being set st X in F holds
IT2 . X = SignGen (f,B,X) ; :: thesis: IT1 = IT2

now :: thesis: for x being object st x in F holds
IT1 . x = IT2 . x

let x be object ; :: thesis: ( x in F implies IT1 . x = IT2 . x )
assume A6: x in F ; :: thesis: IT1 . x = IT2 . x
reconsider X = x as set by A6;
IT1 . x = SignGen (f,B,X) by A4, A6;
hence IT1 . x = IT2 . x by A5, A6; :: thesis: verum

end;

hence IT1 = IT2 by FUNCT_2:12; :: thesis: verum