let X, Y be RealNormSpace; :: thesis: for Z being non empty Subset of X
for v, u being VECTOR of (RealVectSpace (Z,Y))
for f, g being PartFunc of X,Y
for a being Real st dom f = Z & dom g = Z & v = f & u = g holds
( v + u = f + g & a * v = a (#) f )
let Z be non empty Subset of X; :: thesis: for v, u being VECTOR of (RealVectSpace (Z,Y))
for f, g being PartFunc of X,Y
for a being Real st dom f = Z & dom g = Z & v = f & u = g holds
( v + u = f + g & a * v = a (#) f )
let v, u be VECTOR of (RealVectSpace (Z,Y)); :: thesis: for f, g being PartFunc of X,Y
for a being Real st dom f = Z & dom g = Z & v = f & u = g holds
( v + u = f + g & a * v = a (#) f )
let f, g be PartFunc of X,Y; :: thesis: for a being Real st dom f = Z & dom g = Z & v = f & u = g holds
( v + u = f + g & a * v = a (#) f )
let a be Real; :: thesis: ( dom f = Z & dom g = Z & v = f & u = g implies ( v + u = f + g & a * v = a (#) f ) )
assume that
A1: dom f = Z and
A2: dom g = Z and
A3: v = f and
A4: u = g ; :: thesis: ( v + u = f + g & a * v = a (#) f )
A5: dom (f + g) = (dom f) /\ (dom g) by VFUNCT_1:def 1
.= Z by A1, A2 ;
rng (f + g) c= the carrier of Y ;
then f + g is Function of Z, the carrier of Y by A5, FUNCT_2:2;
then reconsider vu = f + g as Element of Funcs (Z, the carrier of Y) by FUNCT_2:8;
for x being Element of Z holds vu . x = (v . x) + (u . x)

proof

let x be Element of Z; :: thesis: vu . x = (v . x) + (u . x)
A6: f /. x = v . x by A1, A3, PARTFUN1:def 6;
A7: g /. x = u . x by A2, A4, PARTFUN1:def 6;
thus vu . x = (f + g) /. x by A5, PARTFUN1:def 6
.= (v . x) + (u . x) by A5, A6, A7, VFUNCT_1:def 1 ; :: thesis: verum

end;

hence v + u = f + g by LOPBAN_1:11; :: thesis: a * v = a (#) f
A8: dom (a (#) f) = Z by A1, VFUNCT_1:def 4;
rng (a (#) f) c= the carrier of Y ;
then a (#) f is Function of Z, the carrier of Y by A8, FUNCT_2:2;
then reconsider av = a (#) f as Element of Funcs (Z, the carrier of Y) by FUNCT_2:8;
for x being Element of Z holds av . x = a * (v . x)

proof

let x be Element of Z; :: thesis: av . x = a * (v . x)
A9: f /. x = v . x by A1, A3, PARTFUN1:def 6;
thus av . x = (a (#) f) /. x by A8, PARTFUN1:def 6
.= a * (v . x) by A8, A9, VFUNCT_1:def 4 ; :: thesis: verum

end;

hence a * v = a (#) f by LOPBAN_1:12; :: thesis: verum