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 = <-> (f1 <//> f2)
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 = <-> (f1 <//> f2)
let f1 be PartFunc of X1,Y1; for f2 being PartFunc of X2,Y2 holds (<-> f1) <//> f2 = <-> (f1 <//> f2)
let f2 be PartFunc of X2,Y2; (<-> f1) <//> f2 = <-> (f1 <//> f2)
set f3 = f1 <//> f2;
set f4 = <-> f1;
A1:
( dom (f1 <//> f2) = (dom f1) /\ (dom f2) & dom (<-> f1) = dom f1 )
by Def33, Def48;
dom ((<-> f1) <//> f2) = (dom (<-> f1)) /\ (dom f2)
by Def48;
hence A2:
dom ((<-> f1) <//> f2) = dom (<-> (f1 <//> f2))
by A1, Def33; FUNCT_1:def 11 for b1 being object holds
( not b1 in dom ((<-> f1) <//> f2) or ((<-> f1) <//> f2) . b1 = (<-> (f1 <//> f2)) . b1 )
let x be object ; ( not x in dom ((<-> f1) <//> f2) or ((<-> f1) <//> f2) . x = (<-> (f1 <//> f2)) . x )
assume A3:
x in dom ((<-> f1) <//> f2)
; ((<-> f1) <//> f2) . x = (<-> (f1 <//> f2)) . x
then A4:
x in dom (f1 <//> f2)
by A1, Def48;
then A5:
x in dom (<-> f1)
by A1, XBOOLE_0:def 4;
thus ((<-> f1) <//> f2) . x =
((<-> f1) . x) /" (f2 . x)
by A3, Def48
.=
(- (f1 . x)) /" (f2 . x)
by A5, Def33
.=
- ((f1 . x) /" (f2 . x))
by Th25
.=
- ((f1 <//> f2) . x)
by A4, Def48
.=
(<-> (f1 <//> f2)) . x
by A2, A3, Def33
; verum