let P1, P2 be Function of D,X; :: thesis: ( ( for d being Element of D holds P1 . d = F . c,d ) & ( for d being Element of D holds P2 . d = F . c,d ) implies P1 = P2 )
assume that
A4: for d being Element of D holds P1 . d = F . c,d and
A5: for d being Element of D holds P2 . d = F . c,d ; :: thesis: P1 = P2

now

let d be set ; :: thesis: ( d in D implies P1 . d = P2 . d )
assume d in D ; :: thesis: P1 . d = P2 . d
then reconsider d1 = d as Element of D ;
P1 . d1 = F . c,d1 by A4;
hence P1 . d = P2 . d by A5; :: thesis: verum

end;

hence P1 = P2 by FUNCT_2:18; :: thesis: verum