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;
A1: ( f1 <##> f = f <##> f1 & f2 <##> f = f <##> f2 ) by Th83;
thus (f1 <++> f2) <##> f = f <##> (f1 <++> f2) by Th83
.= (f1 <##> f) <++> (f2 <##> f) by A1, Th87 ; :: thesis: verum