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 = <-> f2;
A1: ( dom (f1 <//> f2) = (dom f1) /\ (dom f2) & dom (<-> f2) = dom f2 ) by ;
dom (f1 <//> (<-> f2)) = (dom f1) /\ (dom (<-> f2)) by Def48;
hence A2: 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 A3: x in dom (f1 <//> (<-> f2)) ; :: thesis: (f1 <//> (<-> f2)) . x = (<-> (f1 <//> f2)) . x
then A4: x in dom (f1 <//> f2) by ;
then A5: x in dom (<-> f2) by ;
thus (f1 <//> (<-> f2)) . x = (f1 . x) /" ((<-> f2) . x) by
.= (f1 . x) /" (- (f2 . x)) by
.= - ((f1 . x) /" (f2 . x)) by Th27
.= - ((f1 <//> f2) . x) by
.= (<-> (f1 <//> f2)) . x by ; :: thesis: verum