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;
set f5 = <-> f2;
A1:
dom (f1 <++> f2) = (dom f1) /\ (dom f2)
by Def45;
A2:
dom (<-> f2) = dom f2
by Def33;
A3:
dom (<-> (f1 <++> f2)) = dom (f1 <++> f2)
by Def33;
A4:
dom (<-> f1) = dom f1
by Def33;
hence A5:
dom (<-> (f1 <++> f2)) = dom ((<-> f1) <++> (<-> f2))
by A1, A2, A3, Def45; 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 A6:
x in dom (<-> (f1 <++> f2))
; (<-> (f1 <++> f2)) . x = ((<-> f1) <++> (<-> f2)) . x
then A7:
x in dom (<-> f1)
by A1, A4, A3, XBOOLE_0:def 4;
A8:
x in dom (<-> f2)
by A1, A2, A3, A6, XBOOLE_0:def 4;
thus (<-> (f1 <++> f2)) . x =
- ((f1 <++> f2) . x)
by A6, Def33
.=
- ((f1 . x) + (f2 . x))
by A3, A6, Def45
.=
(- (f1 . x)) - (f2 . x)
by Th17
.=
((<-> f1) . x) + (- (f2 . x))
by A7, Def33
.=
((<-> f1) . x) + ((<-> f2) . x)
by A8, Def33
.=
((<-> f1) <++> (<-> f2)) . x
by A5, A6, Def45
; verum