let f1, f2, g be PartFunc of REAL ,REAL ; :: thesis: for C being non empty Subset of REAL holds ((f1 (#) f2) || C) (#) (g || C) = (f1 || C) (#) ((f2 (#) g) || C)
let C be non empty Subset of REAL ; :: thesis: ((f1 (#) f2) || C) (#) (g || C) = (f1 || C) (#) ((f2 (#) g) || C)
A1: ((f1 (#) f2) || C) (#) (g || C) = ((f1 || C) (#) (f2 || C)) (#) (g || C) by INTEGRA5:4;
(f1 || C) (#) ((f2 (#) g) || C) = (f1 || C) (#) ((f2 || C) (#) (g || C)) by INTEGRA5:4;
hence ((f1 (#) f2) || C) (#) (g || C) = (f1 || C) (#) ((f2 (#) g) || C) by A1, RFUNCT_1:21; :: thesis: verum