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)
( ((f1 (#) f2) || C) (#) (g || C) = ((f1 || C) (#) (f2 || C)) (#) (g || C) & (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 RFUNCT_1:9; :: thesis: verum