let X, X1, X2 be set ; :: thesis: for Y, Y1, Y2 being complex-functions-membered set
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2 holds (f1 <--> f2) <//> f = (f1 <//> f) <--> (f2 <//> f)
let Y, Y1, Y2 be complex-functions-membered set ; :: thesis: for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2 holds (f1 <--> f2) <//> f = (f1 <//> f) <--> (f2 <//> f)
let f be PartFunc of X,Y; :: thesis: for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2 holds (f1 <--> f2) <//> f = (f1 <//> f) <--> (f2 <//> f)
let f1 be PartFunc of X1,Y1; :: thesis: for f2 being PartFunc of X2,Y2 holds (f1 <--> f2) <//> f = (f1 <//> f) <--> (f2 <//> f)
let f2 be PartFunc of X2,Y2; :: thesis: (f1 <--> f2) <//> f = (f1 <//> f) <--> (f2 <//> f)
set f3 = f1 <//> f;
set f4 = f2 <//> f;
set f5 = f1 <--> f2;
A4:
dom (f1 <//> f) = (dom f1) /\ (dom f)
by Def47;
A5:
dom (f2 <//> f) = (dom f2) /\ (dom f)
by Def47;
A6:
dom ((f1 <--> f2) <//> f) = (dom f) /\ (dom (f1 <--> f2))
by Def47;
A7:
dom ((f1 <//> f) <--> (f2 <//> f)) = (dom (f1 <//> f)) /\ (dom (f2 <//> f))
by Def45;
dom (f1 <--> f2) = (dom f1) /\ (dom f2)
by Def45;
hence A8:
dom ((f1 <--> f2) <//> f) = dom ((f1 <//> f) <--> (f2 <//> f))
by A7, A4, A5, A6, Th1; :: according to FUNCT_1:def 17 :: thesis: for b1 being set holds
( not b1 in dom ((f1 <--> f2) <//> f) or ((f1 <--> f2) <//> f) . b1 = ((f1 <//> f) <--> (f2 <//> f)) . b1 )
let x be set ; :: thesis: ( not x in dom ((f1 <--> f2) <//> f) or ((f1 <--> f2) <//> f) . x = ((f1 <//> f) <--> (f2 <//> f)) . x )
assume A9:
x in dom ((f1 <--> f2) <//> f)
; :: thesis: ((f1 <--> f2) <//> f) . x = ((f1 <//> f) <--> (f2 <//> f)) . x
then A10:
x in dom (f1 <//> f)
by A7, A8, XBOOLE_0:def 4;
A11:
x in dom (f2 <//> f)
by A7, A9, A8, XBOOLE_0:def 4;
A12:
x in dom (f1 <--> f2)
by A6, A9, XBOOLE_0:def 4;
thus ((f1 <--> f2) <//> f) . x =
((f1 <--> f2) . x) /" (f . x)
by A9, Def47
.=
((f1 . x) - (f2 . x)) /" (f . x)
by A12, Def45
.=
((f1 . x) /" (f . x)) - ((f2 . x) /" (f . x))
by RFUNCT_1:26
.=
((f1 <//> f) . x) - ((f2 . x) /" (f . x))
by A10, Def47
.=
((f1 <//> f) . x) - ((f2 <//> f) . x)
by A11, Def47
.=
((f1 <//> f) <--> (f2 <//> f)) . x
by A9, A8, Def45
; :: thesis: verum