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

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

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

dom (|-- (A,x)) = [#] V
by FUNCT_2:def 1;(|-- (A,x)) . y = 0

let y be object ; :: thesis: ( y in dom (|-- (A,x)) implies (|-- (A,x)) . b_{1} = 0 )

assume y in dom (|-- (A,x)) ; :: thesis: (|-- (A,x)) . b_{1} = 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;

end;assume y in dom (|-- (A,x)) ; :: thesis: (|-- (A,x)) . b

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;

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