let C, D be non empty set ; for F1, F2 being Function of [:C,D:],REAL
for c being Element of C holds ProjMap1 ((F1 + F2),c) = (ProjMap1 (F1,c)) + (ProjMap1 (F2,c))
let F1, F2 be Function of [:C,D:],REAL; for c being Element of C holds ProjMap1 ((F1 + F2),c) = (ProjMap1 (F1,c)) + (ProjMap1 (F2,c))
let c be Element of C; ProjMap1 ((F1 + F2),c) = (ProjMap1 (F1,c)) + (ProjMap1 (F2,c))
( dom (ProjMap1 ((F1 + F2),c)) = D & dom (ProjMap1 (F1,c)) = D & dom (ProjMap1 (F2,c)) = D )
by FUNCT_2:def 1;
then A2:
dom (ProjMap1 ((F1 + F2),c)) = (dom (ProjMap1 (F1,c))) /\ (dom (ProjMap1 (F2,c)))
;
for d being object st d in dom (ProjMap1 ((F1 + F2),c)) holds
(ProjMap1 ((F1 + F2),c)) . d = ((ProjMap1 (F1,c)) . d) + ((ProjMap1 (F2,c)) . d)
proof
let d be
object ;
( d in dom (ProjMap1 ((F1 + F2),c)) implies (ProjMap1 ((F1 + F2),c)) . d = ((ProjMap1 (F1,c)) . d) + ((ProjMap1 (F2,c)) . d) )
assume A3:
d in dom (ProjMap1 ((F1 + F2),c))
;
(ProjMap1 ((F1 + F2),c)) . d = ((ProjMap1 (F1,c)) . d) + ((ProjMap1 (F2,c)) . d)
then A4:
(
(ProjMap1 ((F1 + F2),c)) . d = (F1 + F2) . (
c,
d) &
(ProjMap1 (F1,c)) . d = F1 . (
c,
d) &
(ProjMap1 (F2,c)) . d = F2 . (
c,
d) )
by MESFUNC9:def 6;
reconsider d1 =
d as
Element of
D by A3;
[c,d] in [:C,D:]
by A3, ZFMISC_1:def 2;
then
[c,d] in dom (F1 + F2)
by FUNCT_2:def 1;
hence
(ProjMap1 ((F1 + F2),c)) . d = ((ProjMap1 (F1,c)) . d) + ((ProjMap1 (F2,c)) . d)
by A4, VALUED_1:def 1;
verum
end;
hence
ProjMap1 ((F1 + F2),c) = (ProjMap1 (F1,c)) + (ProjMap1 (F2,c))
by A2, VALUED_1:def 1; verum