let C, D be non empty set ; :: thesis: for F1, F2 being Function of [:C,D:],REAL
for d being Element of D holds ProjMap2 ((F1 + F2),d) = (ProjMap2 (F1,d)) + (ProjMap2 (F2,d))
let F1, F2 be Function of [:C,D:],REAL; :: thesis: for d being Element of D holds ProjMap2 ((F1 + F2),d) = (ProjMap2 (F1,d)) + (ProjMap2 (F2,d))
let d be Element of D; :: thesis: ProjMap2 ((F1 + F2),d) = (ProjMap2 (F1,d)) + (ProjMap2 (F2,d))
( dom (ProjMap2 ((F1 + F2),d)) = C & dom (ProjMap2 (F1,d)) = C & dom (ProjMap2 (F2,d)) = C ) by FUNCT_2:def 1;
then A2: dom (ProjMap2 ((F1 + F2),d)) = (dom (ProjMap2 (F1,d))) /\ (dom (ProjMap2 (F2,d))) ;
for c being object st c in dom (ProjMap2 ((F1 + F2),d)) holds
(ProjMap2 ((F1 + F2),d)) . c = ((ProjMap2 (F1,d)) . c) + ((ProjMap2 (F2,d)) . c)

proof

let c be object ; :: thesis: ( c in dom (ProjMap2 ((F1 + F2),d)) implies (ProjMap2 ((F1 + F2),d)) . c = ((ProjMap2 (F1,d)) . c) + ((ProjMap2 (F2,d)) . c) )
assume A3: c in dom (ProjMap2 ((F1 + F2),d)) ; :: thesis: (ProjMap2 ((F1 + F2),d)) . c = ((ProjMap2 (F1,d)) . c) + ((ProjMap2 (F2,d)) . c)
then A4: ( (ProjMap2 ((F1 + F2),d)) . c = (F1 + F2) . (c,d) & (ProjMap2 (F1,d)) . c = F1 . (c,d) & (ProjMap2 (F2,d)) . c = F2 . (c,d) ) by MESFUNC9:def 7;
reconsider c1 = c as Element of C 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 (ProjMap2 ((F1 + F2),d)) . c = ((ProjMap2 (F1,d)) . c) + ((ProjMap2 (F2,d)) . c) by A4, VALUED_1:def 1; :: thesis: verum

end;

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