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) /\ (dom f2) & dom (<-> f1) = dom f1 ) by Def33, Def47;
dom ((<-> f1) <##> f2) = (dom (<-> f1)) /\ (dom f2) by Def47;
hence A2: dom ((<-> f1) <##> f2) = dom (<-> (f1 <##> f2)) by A1, Def33; :: according to FUNCT_1:def 17 :: thesis: for b₁ being set holds
( not b₁ in proj1 ((<-> f1) <##> f2) or ((<-> f1) <##> f2) . b₁ = (<-> (f1 <##> f2)) . b₁ )
let x be set ; :: thesis: ( not x in proj1 ((<-> 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 A1, Def47;
then A5: x in dom (<-> f1) by A1, XBOOLE_0:def 4;
thus ((<-> f1) <##> f2) . x = ((<-> f1) . x) (#) (f2 . x) by A3, Def47
.= (- (f1 . x)) (#) (f2 . x) by A5, Def33
.= - ((f1 . x) (#) (f2 . x)) by Th25
.= - ((f1 <##> f2) . x) by A4, Def47
.= (<-> (f1 <##> f2)) . x by A2, A3, Def33 ; :: thesis: verum