let f1, f2 be PartFunc of REAL , REAL ; :: thesis: ( dom f1 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds f1 . d = d #R p ) & dom f2 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds f2 . d = d #R p ) implies f1 = f2 )
assume that
A5: ( dom f1 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds f1 . d = d #R p ) ) and
A6: ( dom f2 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds f2 . d = d #R p ) ) ; :: thesis: f1 = f2
for d being Element of REAL st d in right_open_halfline 0 holds
f1 . d = f2 . d

proof

let d be Element of REAL ; :: thesis: ( d in right_open_halfline 0 implies f1 . d = f2 . d )
assume A7: d in right_open_halfline 0 ; :: thesis: f1 . d = f2 . d
thus f1 . d = d #R p by A5, A7
.= f2 . d by A6, A7 ; :: thesis: verum

end;

hence f1 = f2 by A5, A6, PARTFUN1:34; :: thesis: verum