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 :: thesis: for d being object st d in D holds
P1 . d = P2 . d
let d be object ; :: 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 ; :: thesis: verum