let X1, X2 be set ; for Y1, Y2 being complex-functions-membered set
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2 holds f1 <--> f2 = <-> (f2 <--> f1)
let Y1, Y2 be complex-functions-membered set ; for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2 holds f1 <--> f2 = <-> (f2 <--> f1)
let f1 be PartFunc of X1,Y1; for f2 being PartFunc of X2,Y2 holds f1 <--> f2 = <-> (f2 <--> f1)
let f2 be PartFunc of X2,Y2; f1 <--> f2 = <-> (f2 <--> f1)
set f = f2 <--> f1;
A1:
( dom (f1 <--> f2) = (dom f1) /\ (dom f2) & dom (f2 <--> f1) = (dom f2) /\ (dom f1) )
by Def46;
hence A2:
dom (f1 <--> f2) = dom (<-> (f2 <--> f1))
by Def33; FUNCT_1:def 11 for b1 being object holds
( not b1 in dom (f1 <--> f2) or (f1 <--> f2) . b1 = (<-> (f2 <--> f1)) . b1 )
let x be object ; ( not x in dom (f1 <--> f2) or (f1 <--> f2) . x = (<-> (f2 <--> f1)) . x )
assume A3:
x in dom (f1 <--> f2)
; (f1 <--> f2) . x = (<-> (f2 <--> f1)) . x
hence (f1 <--> f2) . x =
(f1 . x) - (f2 . x)
by Def46
.=
- ((f2 . x) - (f1 . x))
by Th18
.=
- ((f2 <--> f1) . x)
by A1, A3, Def46
.=
(<-> (f2 <--> f1)) . x
by A2, A3, Def33
;
verum