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 (#) g) + (f2 (#) g)) || C
let C be non empty Subset of REAL; :: thesis: ((f1 + f2) || C) (#) (g || C) = ((f1 (#) g) + (f2 (#) g)) || C
A1: dom (((f1 (#) g) + (f2 (#) g)) || C) = (dom ((f1 (#) g) + (f2 (#) g))) /\ C by RELAT_1:61
.= ((dom (f1 (#) g)) /\ (dom (f2 (#) g))) /\ C by VALUED_1:def 1
.= (((dom f1) /\ (dom g)) /\ (dom (f2 (#) g))) /\ C by VALUED_1:def 4
.= (((dom f1) /\ (dom g)) /\ ((dom f2) /\ (dom g))) /\ C by VALUED_1:def 4
.= ((dom f1) /\ (((dom g) /\ (dom f2)) /\ (dom g))) /\ C by XBOOLE_1:16
.= ((dom f1) /\ ((dom f2) /\ ((dom g) /\ (dom g)))) /\ C by XBOOLE_1:16
.= (((dom f1) /\ (dom f2)) /\ (dom g)) /\ C by XBOOLE_1:16 ;
A2: dom (((f1 + f2) || C) (#) (g || C)) = (dom ((f1 + f2) || C)) /\ (dom (g || C)) by VALUED_1:def 4
.= ((dom (f1 + f2)) /\ C) /\ (dom (g | C)) by RELAT_1:61
.= ((dom (f1 + f2)) /\ C) /\ ((dom g) /\ C) by RELAT_1:61
.= (((dom f1) /\ (dom f2)) /\ C) /\ ((dom g) /\ C) by VALUED_1:def 1
.= ((dom f1) /\ (dom f2)) /\ ((C /\ (dom g)) /\ C) by XBOOLE_1:16
.= ((dom f1) /\ (dom f2)) /\ ((dom g) /\ (C /\ C)) by XBOOLE_1:16
.= (((dom f1) /\ (dom f2)) /\ (dom g)) /\ C by XBOOLE_1:16 ;
for c being Element of C st c in dom (((f1 + f2) || C) (#) (g || C)) holds
(((f1 + f2) || C) (#) (g || C)) . c = (((f1 (#) g) + (f2 (#) g)) || C) . c

proof

let c be Element of C; :: thesis: ( c in dom (((f1 + f2) || C) (#) (g || C)) implies (((f1 + f2) || C) (#) (g || C)) . c = (((f1 (#) g) + (f2 (#) g)) || C) . c )
assume A3: c in dom (((f1 + f2) || C) (#) (g || C)) ; :: thesis: (((f1 + f2) || C) (#) (g || C)) . c = (((f1 (#) g) + (f2 (#) g)) || C) . c
then A4: c in (dom ((f1 + f2) || C)) /\ (dom (g || C)) by VALUED_1:def 4;
then A5: c in dom (g | C) by XBOOLE_0:def 4;
c in (dom ((f1 (#) g) + (f2 (#) g))) /\ C by A2, A1, A3, RELAT_1:61;
then A6: c in dom ((f1 (#) g) + (f2 (#) g)) by XBOOLE_0:def 4;
then A7: c in (dom (f1 (#) g)) /\ (dom (f2 (#) g)) by VALUED_1:def 1;
then A8: c in dom (f1 (#) g) by XBOOLE_0:def 4;
A9: c in dom ((f1 + f2) | C) by A4, XBOOLE_0:def 4;
then c in (dom (f1 + f2)) /\ C by RELAT_1:61;
then A10: c in dom (f1 + f2) by XBOOLE_0:def 4;
A11: (((f1 + f2) || C) (#) (g || C)) . c = (((f1 + f2) || C) . c) * ((g || C) . c) by A3, VALUED_1:def 4
.= ((f1 + f2) . c) * ((g | C) . c) by A9, FUNCT_1:47
.= ((f1 . c) + (f2 . c)) * ((g | C) . c) by A10, VALUED_1:def 1 ;
A12: c in dom (f2 (#) g) by A7, XBOOLE_0:def 4;
(((f1 (#) g) + (f2 (#) g)) || C) . c = ((f1 (#) g) + (f2 (#) g)) . c by A2, A1, A3, FUNCT_1:47
.= ((f1 (#) g) . c) + ((f2 (#) g) . c) by A6, VALUED_1:def 1
.= ((f1 . c) * (g . c)) + ((f2 (#) g) . c) by A8, VALUED_1:def 4
.= ((f1 . c) * (g . c)) + ((f2 . c) * (g . c)) by A12, VALUED_1:def 4
.= ((f1 . c) + (f2 . c)) * (g . c) ;
hence (((f1 + f2) || C) (#) (g || C)) . c = (((f1 (#) g) + (f2 (#) g)) || C) . c by A5, A11, FUNCT_1:47; :: thesis: verum

end;

hence ((f1 + f2) || C) (#) (g || C) = ((f1 (#) g) + (f2 (#) g)) || C by A2, A1, PARTFUN1:5; :: thesis: verum