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 holds <-> (f1 <--> f2) = (<-> 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 holds <-> (f1 <--> f2) = (<-> f1) <++> f2

let f1 be PartFunc of X1,Y1; :: thesis: for f2 being PartFunc of X2,Y2 holds <-> (f1 <--> f2) = (<-> f1) <++> f2
let f2 be PartFunc of X2,Y2; :: thesis: <-> (f1 <--> f2) = (<-> f1) <++> f2
set f3 = f1 <--> f2;
set f4 = <-> f1;
A1: dom (<-> (f1 <--> f2)) = dom (f1 <--> f2) by Def33;
A2: ( dom (f1 <--> f2) = (dom f1) /\ (dom f2) & dom (<-> f1) = dom f1 ) by ;
hence A3: dom (<-> (f1 <--> f2)) = dom ((<-> f1) <++> f2) by ; :: according to FUNCT_1:def 11 :: thesis: for b1 being object holds
( not b1 in dom (<-> (f1 <--> f2)) or (<-> (f1 <--> f2)) . b1 = ((<-> f1) <++> f2) . b1 )

let x be object ; :: thesis: ( not x in dom (<-> (f1 <--> f2)) or (<-> (f1 <--> f2)) . x = ((<-> f1) <++> f2) . x )
assume A4: x in dom (<-> (f1 <--> f2)) ; :: thesis: (<-> (f1 <--> f2)) . x = ((<-> f1) <++> f2) . x
then A5: x in dom (<-> f1) by ;
thus (<-> (f1 <--> f2)) . x = - ((f1 <--> f2) . x) by
.= - ((f1 . x) - (f2 . x)) by
.= (- (f1 . x)) - (- (f2 . x)) by Th17
.= ((<-> f1) . x) + (f2 . x) by
.= ((<-> f1) <++> f2) . x by ; :: thesis: verum