:: Algebra of Vector Functions :: by Hiroshi Yamazaki and Yasunari Shidama :: :: Received October 27, 1992 :: Copyright (c) 1992-2012 Association of Mizar Users
begin
::
::OPERATIONS ON PARTIAL FUNCTIONS FROM A DOMAIN TO THE SET OF REAL NUMBERS
::
for X being set for C being non emptyset for V being RealNormSpace for f1, f2 being PartFunc of C,V holds ( (f1 + f2)| X =(f1 | X)+(f2 | X) & (f1 + f2)| X =(f1 | X)+ f2 & (f1 + f2)| X = f1 +(f2 | X) )
for X being set for C being non emptyset for V being RealNormSpace for f1, f2 being PartFunc of C,V holds ( (f1 - f2)| X =(f1 | X)-(f2 | X) & (f1 - f2)| X =(f1 | X)- f2 & (f1 - f2)| X = f1 -(f2 | X) )
for X, Y being set for C being non emptyset for V being RealNormSpace for f1, f2 being PartFunc of C,V st f1 | X is V8() & f2 | Y is V8() holds ( (f1 + f2)|(X /\ Y) is V8() & (f1 - f2)|(X /\ Y) is V8() )
::OPERATIONS ON PARTIAL FUNCTIONS FROM A DOMAIN TO THE SET OF REAL NUMBERS
::