let X be non empty set ; :: thesis:
let x be Element of X; :: thesis:
let f1, f2 be Function of X,ExtREAL; :: thesis:

hereby :: thesis:

assume ( f1 is V183() & f2 is V183() ) ; :: thesis:
then reconsider F1 = f1, F2 = f2 as V183() Function of X,ExtREAL ;
dom (F1 + F2) = X by FUNCT_2:def 1;
hence (f1 + f2) . x = (f1 . x) + (f2 . x) by MESFUNC1:def 3; :: thesis:

end;

hereby :: thesis:

assume ( f1 is V184() & f2 is V184() ) ; :: thesis:
then reconsider F1 = f1, F2 = f2 as V184() Function of X,ExtREAL ;
dom (F1 + F2) = X by FUNCT_2:def 1;
hence (f1 + f2) . x = (f1 . x) + (f2 . x) by MESFUNC1:def 3; :: thesis:

end;

hereby :: thesis:

assume A1: ( f1 is V183() & f2 is V184() ) ; :: thesis:
then reconsider F1 = f1 as V183() Function of X,ExtREAL ;
reconsider F2 = f2 as V184() Function of X,ExtREAL by A1;
dom (F1 - F2) = X by FUNCT_2:def 1;
hence (f1 - f2) . x = (f1 . x) - (f2 . x) by MESFUNC1:def 4; :: thesis:

end;

hereby :: thesis:

assume A1: ( f1 is V184() & f2 is V183() ) ; :: thesis:
then reconsider F1 = f1 as V184() Function of X,ExtREAL ;
reconsider F2 = f2 as V183() Function of X,ExtREAL by A1;
dom (F1 - F2) = X by FUNCT_2:def 1;
hence (f1 - f2) . x = (f1 . x) - (f2 . x) by MESFUNC1:def 4; :: thesis:

end;