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 :: thesis: for c being object st c in C holds
P1 . c = P2 . c

let c be object ; :: 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 ; :: thesis: verum