let C, D be non empty set ; :: thesis: 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; :: thesis: for c being Element of C holds ProjMap1 ((F1 + F2),c) = (ProjMap1 (F1,c)) + (ProjMap1 (F2,c))
let c be Element of C; :: thesis: 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 ; :: thesis: ( 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)) ; :: thesis: (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; :: thesis: verum

end;

hence ProjMap1 ((F1 + F2),c) = (ProjMap1 (F1,c)) + (ProjMap1 (F2,c)) by A2, VALUED_1:def 1; :: thesis: verum