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)) . b1 = 0 )
assume y in dom (|-- (A,x)) ; :: thesis: (|-- (A,x)) . b1 = 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)) . b1 = 0
hence (|-- (A,x)) . y = 0 by ; :: thesis: verum
end;
suppose not x in [#] V ; :: thesis: (|-- (A,x)) . b1 = 0
then not x in dom (y |-- A) ;
hence (|-- (A,x)) . y = 0 by ; :: thesis: verum
end;
end;
end;
dom (|-- (A,x)) = [#] V by FUNCT_2:def 1;
hence |-- (A,x) = ([#] V) --> 0 by ; :: thesis: verum