let X, X1 be set ; :: thesis: for Y, Y1 being complex-functions-membered set
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1 st f1 = <-> f holds
<-> f1 = f
let Y, Y1 be complex-functions-membered set ; :: thesis: for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1 st f1 = <-> f holds
<-> f1 = f
let f be PartFunc of X,Y; :: thesis: for f1 being PartFunc of X1,Y1 st f1 = <-> f holds
<-> f1 = f
let f1 be PartFunc of X1,Y1; :: thesis: ( f1 = <-> f implies <-> f1 = f )
assume A1: f1 = <-> f ; :: thesis: <-> f1 = f
then A2: dom f1 = dom f by Def32;
hence A3: dom (<-> f1) = dom f by Def32; :: according to FUNCT_1:def 17 :: thesis: for b₁ being set holds
( not b₁ in dom (<-> f1) or (<-> f1) . b₁ = f . b₁ )
let x be set ; :: thesis: ( not x in dom (<-> f1) or (<-> f1) . x = f . x )
assume A4: x in dom (<-> f1) ; :: thesis: (<-> f1) . x = f . x
hence (<-> f1) . x = - (f1 . x) by Def32
.= - (- (f . x)) by A1, A2, A3, A4, Def32
.= f . x ;
:: thesis: verum