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 and
A6: for d being Element of right_open_halfline 0 holds f1 . d = d #R p and
A7: dom f2 = right_open_halfline 0 and
A8: 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 A9: d in right_open_halfline 0 ; :: thesis: f1 . d = f2 . d
thus f1 . d = d #R p by A6, A9
.= f2 . d by A8, A9 ; :: thesis: verum
end;
hence f1 = f2 by A5, A7, PARTFUN1:5; :: thesis: verum