let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for x being Element of M st f1 is total & f2 is total holds
( (f1 + f2) /. x = (f1 /. x) + (f2 /. x) & (f1 - f2) /. x = (f1 /. x) - (f2 /. x) )
let V be ComplexNormSpace; :: thesis: for f1, f2 being PartFunc of M,V
for x being Element of M st f1 is total & f2 is total holds
( (f1 + f2) /. x = (f1 /. x) + (f2 /. x) & (f1 - f2) /. x = (f1 /. x) - (f2 /. x) )
let f1, f2 be PartFunc of M,V; :: thesis: for x being Element of M st f1 is total & f2 is total holds
( (f1 + f2) /. x = (f1 /. x) + (f2 /. x) & (f1 - f2) /. x = (f1 /. x) - (f2 /. x) )
let x be Element of M; :: thesis: ( f1 is total & f2 is total implies ( (f1 + f2) /. x = (f1 /. x) + (f2 /. x) & (f1 - f2) /. x = (f1 /. x) - (f2 /. x) ) )
assume A1: ( f1 is total & f2 is total ) ; :: thesis: ( (f1 + f2) /. x = (f1 /. x) + (f2 /. x) & (f1 - f2) /. x = (f1 /. x) - (f2 /. x) )
then f1 + f2 is total by Th32;
then dom (f1 + f2) = M ;
hence (f1 + f2) /. x = (f1 /. x) + (f2 /. x) by VFUNCT_1:def 1; :: thesis: (f1 - f2) /. x = (f1 /. x) - (f2 /. x)
f1 - f2 is total by A1, Th32;
then dom (f1 - f2) = M ;
hence (f1 - f2) /. x = (f1 /. x) - (f2 /. x) by VFUNCT_1:def 2; :: thesis: verum