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

now

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

end;

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