let x be set ; :: thesis: for V being RealLinearSpace
for A being Subset of V st not x in A holds
|-- (A,x) = ([#] V) --> 0
let V be RealLinearSpace; :: thesis: for A being Subset of V st not x in A holds
|-- (A,x) = ([#] V) --> 0
let A be Subset of V; :: thesis: ( not x in A implies |-- (A,x) = ([#] V) --> 0 )
set Ax = |-- (A,x);
assume A1: not x in A ; :: thesis: |-- (A,x) = ([#] V) --> 0

A2: now :: thesis: for y being object st y in dom (|-- (A,x)) holds
(|-- (A,x)) . y = 0

let y be object ; :: thesis: ( y in dom (|-- (A,x)) implies (|-- (A,x)) . b₁ = 0 )
assume y in dom (|-- (A,x)) ; :: thesis: (|-- (A,x)) . b₁ = 0
then A3: (|-- (A,x)) . y = (y |-- A) . x by Def3;
Carrier (y |-- A) c= A by RLVECT_2:def 6;
then A4: not x in Carrier (y |-- A) by A1;

per cases ( x in [#] V or not x in [#] V ) ;

suppose x in [#] V ; :: thesis: (|-- (A,x)) . b₁ = 0

hence (|-- (A,x)) . y = 0 by A3, A4, RLVECT_2:19; :: thesis: verum

end;

suppose not x in [#] V ; :: thesis: (|-- (A,x)) . b₁ = 0

then not x in dom (y |-- A) ;
hence (|-- (A,x)) . y = 0 by A3, FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

dom (|-- (A,x)) = [#] V by FUNCT_2:def 1;
hence |-- (A,x) = ([#] V) --> 0 by A2, FUNCOP_1:11; :: thesis: verum