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