let X1, X2, X3, X4 be set ; :: thesis: for Y1, Y2, Y3, Y4 being complex-functions-membered set
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2
for f3 being PartFunc of X3,Y3
for f4 being PartFunc of X4,Y4 st f3 = f1 <//> f2 & f4 = <-> f1 holds
f4 <//> f2 = <-> f3
let Y1, Y2, Y3, Y4 be complex-functions-membered set ; :: thesis: for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2
for f3 being PartFunc of X3,Y3
for f4 being PartFunc of X4,Y4 st f3 = f1 <//> f2 & f4 = <-> f1 holds
f4 <//> f2 = <-> f3
let f1 be PartFunc of X1,Y1; :: thesis: for f2 being PartFunc of X2,Y2
for f3 being PartFunc of X3,Y3
for f4 being PartFunc of X4,Y4 st f3 = f1 <//> f2 & f4 = <-> f1 holds
f4 <//> f2 = <-> f3
let f2 be PartFunc of X2,Y2; :: thesis: for f3 being PartFunc of X3,Y3
for f4 being PartFunc of X4,Y4 st f3 = f1 <//> f2 & f4 = <-> f1 holds
f4 <//> f2 = <-> f3
let f3 be PartFunc of X3,Y3; :: thesis: for f4 being PartFunc of X4,Y4 st f3 = f1 <//> f2 & f4 = <-> f1 holds
f4 <//> f2 = <-> f3
let f4 be PartFunc of X4,Y4; :: thesis: ( f3 = f1 <//> f2 & f4 = <-> f1 implies f4 <//> f2 = <-> f3 )
assume that
A1: f3 = f1 <//> f2 and
A2: f4 = <-> f1 ; :: thesis: f4 <//> f2 = <-> f3
A4: dom f3 = (dom f1) /\ (dom f2) by A1, Def47;
A5: dom f4 = dom f1 by A2, Def32;
dom (f4 <//> f2) = (dom f4) /\ (dom f2) by Def47;
hence A8: dom (f4 <//> f2) = dom (<-> f3) by A4, A5, Def32; :: according to FUNCT_1:def 17 :: thesis: for b₁ being set holds
( not b₁ in dom (f4 <//> f2) or (f4 <//> f2) . b₁ = (<-> f3) . b₁ )
let x be set ; :: thesis: ( not x in dom (f4 <//> f2) or (f4 <//> f2) . x = (<-> f3) . x )
assume A9: x in dom (f4 <//> f2) ; :: thesis: (f4 <//> f2) . x = (<-> f3) . x
then A10: x in dom f3 by A4, A5, Def47;
then A11: x in dom (<-> f1) by A2, A4, A5, XBOOLE_0:def 4;
thus (f4 <//> f2) . x = (f4 . x) /" (f2 . x) by A9, Def47
.= (- (f1 . x)) /" (f2 . x) by A2, A11, Def32
.= - ((f1 . x) /" (f2 . x)) by Th13b
.= - (f3 . x) by A1, A10, Def47
.= (<-> f3) . x by A9, A8, Def32 ; :: thesis: verum