let F be Field; :: thesis: for S being SymSp of F
for b, a, x being Element of S
for l being Element of F st not a _|_ & l <> 0. F holds
ProJ (l * a),b,x = ProJ a,b,x
let S be SymSp of F; :: thesis: for b, a, x being Element of S
for l being Element of F st not a _|_ & l <> 0. F holds
ProJ (l * a),b,x = ProJ a,b,x
let b, a, x be Element of S; :: thesis: for l being Element of F st not a _|_ & l <> 0. F holds
ProJ (l * a),b,x = ProJ a,b,x
let l be Element of F; :: thesis: ( not a _|_ & l <> 0. F implies ProJ (l * a),b,x = ProJ a,b,x )
assume that
A1: not a _|_ and
A2: l <> 0. F ; :: thesis: ProJ (l * a),b,x = ProJ a,b,x
not l * a _|_ by A1, A2, Th15;
then l * a _|_ by Th27;
then x - ((ProJ (l * a),b,x) * b) _|_ by Th12;
then x - ((ProJ (l * a),b,x) * b) _|_ by Def1;
then x - ((ProJ (l * a),b,x) * b) _|_ by VECTSP_1:def 28;
then x - ((ProJ (l * a),b,x) * b) _|_ by A2, VECTSP_1:def 22;
then x - ((ProJ (l * a),b,x) * b) _|_ by VECTSP_1:def 29;
then A3: a _|_ by Th12;
a _|_ by A1, Th27;
hence ProJ (l * a),b,x = ProJ a,b,x by A1, A3, Th24; :: thesis: verum