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 + 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:90
.=
((dom (f1 + f2)) /\ C) /\ ((dom g) /\ C)
by RELAT_1:90
.=
(((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
;
A2: dom (((f1 (#) g) + (f2 (#) g)) || C) =
(dom ((f1 (#) g) + (f2 (#) g))) /\ C
by RELAT_1:90
.=
((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
;
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
c in (dom ((f1 + f2) || C)) /\ (dom (g || C))
by VALUED_1:def 4;
then A4:
(
c in dom ((f1 + f2) | C) &
c in dom (g | C) )
by XBOOLE_0:def 4;
then
(
c in (dom (f1 + f2)) /\ C &
c in dom (g | C) )
by RELAT_1:90;
then A5:
(
c in dom (f1 + f2) &
c in dom (g | C) )
by XBOOLE_0:def 4;
A6:
(((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 A4, FUNCT_1:70
.=
((f1 . c) + (f2 . c)) * ((g | C) . c)
by A5, VALUED_1:def 1
;
c in (dom ((f1 (#) g) + (f2 (#) g))) /\ C
by A1, A2, A3, RELAT_1:90;
then A7:
c in dom ((f1 (#) g) + (f2 (#) g))
by XBOOLE_0:def 4;
then
c in (dom (f1 (#) g)) /\ (dom (f2 (#) g))
by VALUED_1:def 1;
then A8:
(
c in dom (f1 (#) g) &
c in dom (f2 (#) g) )
by XBOOLE_0:def 4;
(((f1 (#) g) + (f2 (#) g)) || C) . c =
((f1 (#) g) + (f2 (#) g)) . c
by A1, A2, A3, FUNCT_1:70
.=
((f1 (#) g) . c) + ((f2 (#) g) . c)
by A7, 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 A8, VALUED_1:def 4
.=
((f1 . c) + (f2 . c)) * (g . c)
;
hence
(((f1 + f2) || C) (#) (g || C)) . c = (((f1 (#) g) + (f2 (#) g)) || C) . c
by A4, A6, FUNCT_1:70;
:: thesis: verum
end;
hence
((f1 + f2) || C) (#) (g || C) = ((f1 (#) g) + (f2 (#) g)) || C
by A1, A2, PARTFUN1:34; :: thesis: verum