let f1, f2, g be PartFunc of REAL,REAL; 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; ((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;
( 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))
;
(((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;
verum
end;
hence
((f1 + f2) || C) (#) (g || C) = ((f1 (#) g) + (f2 (#) g)) || C
by A2, A1, PARTFUN1:5; verum