let X1, X2 be set ; :: thesis: for Y1, Y2 being complex-functions-membered set
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2 st <-> f1 = <-> f2 holds
f1 = f2
let Y1, Y2 be complex-functions-membered set ; :: thesis: for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2 st <-> f1 = <-> f2 holds
f1 = f2
let f1 be PartFunc of X1,Y1; :: thesis: for f2 being PartFunc of X2,Y2 st <-> f1 = <-> f2 holds
f1 = f2
let f2 be PartFunc of X2,Y2; :: thesis: ( <-> f1 = <-> f2 implies f1 = f2 )
A1: dom (<-> f1) = dom f1 by Def33;
assume A2: <-> f1 = <-> f2 ; :: thesis: f1 = f2
hence dom f1 = dom f2 by A1, Def33; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom f1 or f1 . b₁ = f2 . b₁ )
let x be object ; :: thesis: ( not x in dom f1 or f1 . x = f2 . x )
assume A3: x in dom f1 ; :: thesis: f1 . x = f2 . x
thus f1 . x = - (- (f1 . x))
.= - ((<-> f1) . x) by A1, A3, Def33
.= - (- (f2 . x)) by A2, A1, A3, Def33
.= f2 . x ; :: thesis: verum