:: VECTSP10 semantic presentation

definition

let c₁ be doubleLoopStr ;
func StructVectSp c₁ -> strict VectSpStr of a₁ equals :: VECTSP10:def 1
VectSpStr(# the carrier of a₁,the add of a₁,the Zero of a₁,the mult of a₁ #);
coherence ;

end;

:: deftheorem Def1 defines StructVectSp VECTSP10:def 1 :

registration

let c₁ be non empty doubleLoopStr ;
cluster StructVectSp a₁ -> non empty strict ;
coherence ;

end;

registration

let c₁ be non empty Abelian doubleLoopStr ;
cluster StructVectSp a₁ -> non empty Abelian strict ;
coherence

proof end;

end;

registration

let c₁ be non empty add-associative doubleLoopStr ;
cluster StructVectSp a₁ -> non empty add-associative strict ;
coherence

proof end;

end;

registration

let c₁ be non empty right_zeroed doubleLoopStr ;
cluster StructVectSp a₁ -> non empty right_zeroed strict ;
coherence

proof end;

end;

registration

let c₁ be non empty right_complementable doubleLoopStr ;
cluster StructVectSp a₁ -> non empty right_complementable strict ;
coherence

proof end;

end;

registration

let c₁ be non empty associative distributive left_unital doubleLoopStr ;
cluster StructVectSp a₁ -> non empty strict VectSp-like ;
coherence

proof end;

end;

registration

let c₁ be non empty non degenerated doubleLoopStr ;
cluster StructVectSp a₁ -> non empty strict non trivial ;
coherence

proof end;

end;

registration

let c₁ be non empty non degenerated doubleLoopStr ;
cluster non empty non trivial VectSpStr of a₁;
existence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable doubleLoopStr ;
cluster non empty add-associative right_zeroed right_complementable strict VectSpStr of a₁;
correctness

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
cluster non empty add-associative right_zeroed right_complementable strict VectSp-like VectSpStr of a₁;
correctness

proof end;

end;

registration

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital non degenerated doubleLoopStr ;
cluster non empty Abelian add-associative right_zeroed right_complementable strict VectSp-like non trivial VectSpStr of a₁;
existence

proof end;

end;

theorem Th1: :: VECTSP10:1

canceled;

theorem Th2: :: VECTSP10:2

for b₁ being non empty add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being Element of b₁
for b₃ being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₄ being Vector of b₃ holds
( (0. b₁) * b₄ = 0. b₃ & b₂ * (0. b₃) = 0. b₃ )

proof end;

theorem Th3: :: VECTSP10:3

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being VectSp of b₁
for b₃, b₄ being Subspace of b₂
for b₅ being Vector of b₂ st b₃ /\ b₄ = (0). b₂ & b₅ in b₃ & b₅ in b₄ holds
b₅ = 0. b₂

proof end;

theorem Th4: :: VECTSP10:4

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being set
for b₄ being Vector of b₂ holds
( b₃ in Lin {b₄} iff ex b₅ being Element of b₁ st b₃ = b₅ * b₄ )

proof end;

theorem Th5: :: VECTSP10:5

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Vector of b₂
for b₄, b₅ being Scalar of st b₃ <> 0. b₂ & b₄ * b₃ = b₅ * b₃ holds
b₄ = b₅

proof end;

theorem Th6: :: VECTSP10:6

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being VectSp of b₁
for b₃, b₄ being Subspace of b₂ st b₂ is_the_direct_sum_of b₃,b₄ holds
for b₅, b₆, b₇ being Vector of b₂ st b₆ in b₃ & b₇ in b₄ & b₅ = b₆ + b₇ holds
b₅ |-- b₃,b₄ = [b₆,b₇]

proof end;

theorem Th7: :: VECTSP10:7

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being VectSp of b₁
for b₃, b₄ being Subspace of b₂ st b₂ is_the_direct_sum_of b₃,b₄ holds
for b₅, b₆, b₇ being Vector of b₂ st b₅ |-- b₃,b₄ = [b₆,b₇] holds
b₅ = b₆ + b₇

proof end;

theorem Th8: :: VECTSP10:8

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being VectSp of b₁
for b₃, b₄ being Subspace of b₂ st b₂ is_the_direct_sum_of b₃,b₄ holds
for b₅, b₆, b₇ being Vector of b₂ st b₅ |-- b₃,b₄ = [b₆,b₇] holds
( b₆ in b₃ & b₇ in b₄ )

proof end;

theorem Th9: :: VECTSP10:9

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being VectSp of b₁
for b₃, b₄ being Subspace of b₂ st b₂ is_the_direct_sum_of b₃,b₄ holds
for b₅, b₆, b₇ being Vector of b₂ st b₅ |-- b₃,b₄ = [b₆,b₇] holds
b₅ |-- b₄,b₃ = [b₇,b₆]

proof end;

theorem Th10: :: VECTSP10:10

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being VectSp of b₁
for b₃, b₄ being Subspace of b₂ st b₂ is_the_direct_sum_of b₃,b₄ holds
for b₅ being Vector of b₂ st b₅ in b₃ holds
b₅ |-- b₃,b₄ = [b₅,(0. b₂)]

proof end;

theorem Th11: :: VECTSP10:11

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being VectSp of b₁
for b₃, b₄ being Subspace of b₂ st b₂ is_the_direct_sum_of b₃,b₄ holds
for b₅ being Vector of b₂ st b₅ in b₄ holds
b₅ |-- b₃,b₄ = [(0. b₂),b₅]

proof end;

theorem Th12: :: VECTSP10:12

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being VectSp of b₁
for b₃ being Subspace of b₂
for b₄ being Subspace of b₃
for b₅ being Vector of b₂ st b₅ in b₄ holds
b₅ is Vector of b₃

proof end;

theorem Th13: :: VECTSP10:13

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being VectSp of b₁
for b₃, b₄, b₅ being Subspace of b₂
for b₆, b₇ being Subspace of b₅ st b₆ = b₃ & b₇ = b₄ holds
b₆ + b₇ = b₃ + b₄

proof end;

theorem Th14: :: VECTSP10:14

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Subspace of b₂
for b₄ being Vector of b₂
for b₅ being Vector of b₃ st b₄ = b₅ holds
Lin {b₅} = Lin {b₄}

proof end;

theorem Th15: :: VECTSP10:15

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Vector of b₂
for b₄ being Subspace of b₂ st not b₃ in b₄ holds
for b₅ being Vector of (b₄ + (Lin {b₃}))
for b₆ being Subspace of b₄ + (Lin {b₃}) st b₃ = b₅ & b₆ = b₄ holds
b₄ + (Lin {b₃}) is_the_direct_sum_of b₆, Lin {b₅}

proof end;

theorem Th16: :: VECTSP10:16

proof end;

theorem Th17: :: VECTSP10:17

proof end;

theorem Th18: :: VECTSP10:18

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being VectSp of b₁
for b₃ being Vector of b₂
for b₄, b₅ being Subspace of b₂ ex b₆, b₇ being Vector of b₂ st b₃ |-- b₄,b₅ = [b₆,b₇]

proof end;

theorem Th19: :: VECTSP10:19

proof end;

theorem Th20: :: VECTSP10:20

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Vector of b₂
for b₄ being Subspace of b₂
for b₅ being Vector of (b₄ + (Lin {b₃}))
for b₆ being Subspace of b₄ + (Lin {b₃}) st b₃ = b₅ & b₄ = b₆ & not b₃ in b₄ holds
for b₇, b₈ being Vector of (b₄ + (Lin {b₃}))
for b₉, b₁₀ being Vector of b₄
for b₁₁, b₁₂ being Element of b₁ st b₇ |-- b₆,(Lin {b₅}) = [b₉,(b₁₁ * b₃)] & b₈ |-- b₆,(Lin {b₅}) = [b₁₀,(b₁₂ * b₃)] holds
(b₇ + b₈) |-- b₆,(Lin {b₅}) = [(b₉ + b₁₀),((b₁₁ + b₁₂) * b₃)]

proof end;

theorem Th21: :: VECTSP10:21

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Vector of b₂
for b₄ being Subspace of b₂
for b₅ being Vector of (b₄ + (Lin {b₃}))
for b₆ being Subspace of b₄ + (Lin {b₃}) st b₃ = b₅ & b₄ = b₆ & not b₃ in b₄ holds
for b₇ being Vector of (b₄ + (Lin {b₃}))
for b₈ being Vector of b₄
for b₉, b₁₀ being Element of b₁ st b₇ |-- b₆,(Lin {b₅}) = [b₈,(b₁₀ * b₃)] holds
(b₉ * b₇) |-- b₆,(Lin {b₅}) = [(b₉ * b₈),((b₉ * b₁₀) * b₃)]

proof end;

definition

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂ be VectSp of c₁;
let c₃ be Subspace of c₂;
func CosetSet c₂,c₃ -> non empty Subset-Family of a₂ equals :: VECTSP10:def 2
{ b₁ where B is Coset of a₃ : verum } ;
correctness

proof end;

end;

:: deftheorem Def2 defines CosetSet VECTSP10:def 2 :

definition

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂ be VectSp of c₁;
let c₃ be Subspace of c₂;
func addCoset c₂,c₃ -> BinOp of CosetSet a₂,a₃ means :Def3: :: VECTSP10:def 3
for b₁, b₂ being Element of CosetSet a₂,a₃
for b₃, b₄ being Vector of a₂ st b₁ = b₃ + a₃ & b₂ = b₄ + a₃ holds
a₄ . b₁,b₂ = (b₃ + b₄) + a₃;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines addCoset VECTSP10:def 3 :

definition

proof end;

end;

:: deftheorem Def4 defines zeroCoset VECTSP10:def 4 :

definition

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂ be VectSp of c₁;
let c₃ be Subspace of c₂;
func lmultCoset c₂,c₃ -> Function of [:the carrier of a₁,(CosetSet a₂,a₃):], CosetSet a₂,a₃ means :Def5: :: VECTSP10:def 5
for b₁ being Element of a₁
for b₂ being Element of CosetSet a₂,a₃
for b₃ being Vector of a₂ st b₂ = b₃ + a₃ holds
a₄ . b₁,b₂ = (b₁ * b₃) + a₃;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines lmultCoset VECTSP10:def 5 :

definition

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂ be VectSp of c₁;
let c₃ be Subspace of c₂;
func VectQuot c₂,c₃ -> non empty Abelian add-associative right_zeroed right_complementable strict VectSp-like VectSpStr of a₁ means :Def6: :: VECTSP10:def 6
( the carrier of a₄ = CosetSet a₂,a₃ & the add of a₄ = addCoset a₂,a₃ & the Zero of a₄ = zeroCoset a₂,a₃ & the lmult of a₄ = lmultCoset a₂,a₃ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def6 defines VectQuot VECTSP10:def 6 :

theorem Th22: :: VECTSP10:22

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being VectSp of b₁
for b₃ being Subspace of b₂ holds
( zeroCoset b₂,b₃ = (0. b₂) + b₃ & 0. (VectQuot b₂,b₃) = zeroCoset b₂,b₃ )

proof end;

theorem Th23: :: VECTSP10:23

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being VectSp of b₁
for b₃ being Subspace of b₂
for b₄ being Vector of (VectQuot b₂,b₃) holds
( b₄ is Coset of b₃ & ex b₅ being Vector of b₂ st b₄ = b₅ + b₃ )

proof end;

theorem Th24: :: VECTSP10:24

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being VectSp of b₁
for b₃ being Subspace of b₂
for b₄ being Vector of b₂ holds
( b₄ + b₃ is Coset of b₃ & b₄ + b₃ is Vector of (VectQuot b₂,b₃) )

proof end;

theorem Th25: :: VECTSP10:25

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being VectSp of b₁
for b₃ being Subspace of b₂
for b₄ being Coset of b₃ holds b₄ is Vector of (VectQuot b₂,b₃)

proof end;

theorem Th26: :: VECTSP10:26

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being VectSp of b₁
for b₃ being Subspace of b₂
for b₄ being Vector of (VectQuot b₂,b₃)
for b₅ being Vector of b₂
for b₆ being Scalar of st b₄ = b₅ + b₃ holds
b₆ * b₄ = (b₆ * b₅) + b₃

proof end;

theorem Th27: :: VECTSP10:27

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being VectSp of b₁
for b₃ being Subspace of b₂
for b₄, b₅ being Vector of (VectQuot b₂,b₃)
for b₆, b₇ being Vector of b₂ st b₄ = b₆ + b₃ & b₅ = b₇ + b₃ holds
b₄ + b₅ = (b₆ + b₇) + b₃

proof end;

theorem Th28: :: VECTSP10:28

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Subspace of b₂
for b₄ being linear-Functional of b₃
for b₅ being Vector of b₂
for b₆ being Vector of (b₃ + (Lin {b₅})) st b₅ = b₆ & not b₅ in b₃ holds
for b₇ being Element of b₁ ex b₈ being linear-Functional of (b₃ + (Lin {b₅})) st
( b₈ | the carrier of b₃ = b₄ & b₈ . b₆ = b₇ )

proof end;

registration

let c₁ be non empty right_zeroed LoopStr ;
let c₂ be non empty VectSpStr of c₁;
cluster additive 0-preserving Relation of the carrier of a₂,the carrier of a₁;
existence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable doubleLoopStr ;
let c₂ be non empty right_zeroed VectSpStr of c₁;
cluster additive -> 0-preserving Relation of the carrier of a₂,the carrier of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂ be non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of c₁;
cluster homogeneous -> 0-preserving Relation of the carrier of a₂,the carrier of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty ZeroStr ;
let c₂ be non empty VectSpStr of c₁;
cluster 0Functional a₂ -> constant ;
coherence

proof end;

end;

registration

let c₁ be non empty ZeroStr ;
let c₂ be non empty VectSpStr of c₁;
cluster constant Relation of the carrier of a₂,the carrier of a₁;
existence

proof end;

end;

definition

let c₁ be non empty add-associative right_zeroed right_complementable doubleLoopStr ;
let c₂ be non empty right_zeroed VectSpStr of c₁;
let c₃ be 0-preserving Functional of c₂;
redefine attr constant as a₃ is constant means :Def7: :: VECTSP10:def 7
a₃ = 0Functional a₂;
compatibility

proof end;

end;

:: deftheorem Def7 defines constant VECTSP10:def 7 :

registration

let c₁ be non empty add-associative right_zeroed right_complementable doubleLoopStr ;
let c₂ be non empty right_zeroed VectSpStr of c₁;
cluster constant additive 0-preserving Relation of the carrier of a₂,the carrier of a₁;
existence

proof end;

end;

registration

let c₁ be non empty 1-sorted ;
let c₂ be non empty VectSpStr of c₁;
cluster non constant -> non trivial Relation of the carrier of a₂,the carrier of a₁;
coherence

proof end;

end;

registration

let c₁ be Field;
let c₂ be non trivial VectSp of c₁;
cluster non constant additive homogeneous 0-preserving non trivial Relation of the carrier of a₂,the carrier of a₁;
existence

proof end;

end;

registration

let c₁ be Field;
let c₂ be non trivial VectSp of c₁;
cluster trivial -> constant Relation of the carrier of a₂,the carrier of a₁;
coherence

proof end;

end;

definition

let c₁ be Field;
let c₂ be non trivial VectSp of c₁;
let c₃ be Vector of c₂;
let c₄ be Linear_Compl of Lin {c₃};
assume E28: c₃ <> 0. c₂ ;
func coeffFunctional c₃,c₄ -> V71 non trivial linear-Functional of a₂ means :Def8: :: VECTSP10:def 8
( a₅ . a₃ = 1. a₁ & a₅ | the carrier of a₄ = 0Functional a₄ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines coeffFunctional VECTSP10:def 8 :

theorem Th29: :: VECTSP10:29

for b₁ being Field
for b₂ being non trivial VectSp of b₁
for b₃ being non constant 0-preserving Functional of b₂ ex b₄ being Vector of b₂ st
( b₄ <> 0. b₂ & b₃ . b₄ <> 0. b₁ )

proof end;

theorem Th30: :: VECTSP10:30

for b₁ being Field
for b₂ being non trivial VectSp of b₁
for b₃ being Vector of b₂
for b₄ being Scalar of
for b₅ being Linear_Compl of Lin {b₃} st b₃ <> 0. b₂ holds
(coeffFunctional b₃,b₅) . (b₄ * b₃) = b₄

proof end;

theorem Th31: :: VECTSP10:31

for b₁ being Field
for b₂ being non trivial VectSp of b₁
for b₃, b₄ being Vector of b₂
for b₅ being Linear_Compl of Lin {b₃} st b₃ <> 0. b₂ & b₄ in b₅ holds
(coeffFunctional b₃,b₅) . b₄ = 0. b₁

proof end;

theorem Th32: :: VECTSP10:32

for b₁ being Field
for b₂ being non trivial VectSp of b₁
for b₃, b₄ being Vector of b₂
for b₅ being Scalar of
for b₆ being Linear_Compl of Lin {b₃} st b₃ <> 0. b₂ & b₄ in b₆ holds
(coeffFunctional b₃,b₆) . ((b₅ * b₃) + b₄) = b₅

proof end;

theorem Th33: :: VECTSP10:33

for b₁ being non empty LoopStr
for b₂ being non empty VectSpStr of b₁
for b₃, b₄ being Functional of b₂
for b₅ being Vector of b₂ holds (b₃ - b₄) . b₅ = (b₃ . b₅) - (b₄ . b₅)

proof end;

registration

let c₁ be Field;
let c₂ be non trivial VectSp of c₁;
cluster a₂ *' -> non trivial ;
coherence

proof end;

end;

definition

let c₁ be non empty ZeroStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃ be Functional of c₂;
func ker c₃ -> Subset of a₂ equals :: VECTSP10:def 9
{ b₁ where B is Vector of a₂ : a₃ . b₁ = 0. a₁ } ;
coherence

proof end;

end;

:: deftheorem Def9 defines ker VECTSP10:def 9 :

registration

let c₁ be non empty right_zeroed LoopStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃ be 0-preserving Functional of c₂;
cluster ker a₃ -> non empty ;
coherence

proof end;

end;

theorem Th34: :: VECTSP10:34

for b₁ being non empty add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃ being linear-Functional of b₂ holds ker b₃ is lineary-closed

proof end;

definition

let c₁ be non empty ZeroStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃ be Functional of c₂;
attr a₃ is degenerated means :Def10: :: VECTSP10:def 10
ker a₃ <> {(0. a₂)};

end;

:: deftheorem Def10 defines degenerated VECTSP10:def 10 :

registration

let c₁ be non empty non degenerated doubleLoopStr ;
let c₂ be non empty non trivial VectSpStr of c₁;
cluster 0-preserving non degenerated -> non constant non trivial Relation of the carrier of a₂,the carrier of a₁;
coherence

proof end;

end;

definition

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂ be VectSp of c₁;
let c₃ be linear-Functional of c₂;
func Ker c₃ -> non empty strict Subspace of a₂ means :Def11: :: VECTSP10:def 11
the carrier of a₄ = ker a₃;
existence

proof end;

uniqueness by VECTSP_4:37;

end;

:: deftheorem Def11 defines Ker VECTSP10:def 11 :

definition

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂ be VectSp of c₁;
let c₃ be Subspace of c₂;
let c₄ be additive Functional of c₂;
assume E35: the carrier of c₃ c= ker c₄ ;
func QFunctional c₄,c₃ -> additive Functional of (VectQuot a₂,a₃) means :Def12: :: VECTSP10:def 12
for b₁ being Vector of (VectQuot a₂,a₃)
for b₂ being Vector of a₂ st b₁ = b₂ + a₃ holds
a₅ . b₁ = a₄ . b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines QFunctional VECTSP10:def 12 :

theorem Th35: :: VECTSP10:35

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being VectSp of b₁
for b₃ being Subspace of b₂
for b₄ being linear-Functional of b₂ st the carrier of b₃ c= ker b₄ holds
QFunctional b₄,b₃ is homogeneous

proof end;

definition

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂ be VectSp of c₁;
let c₃ be linear-Functional of c₂;
func CQFunctional c₃ -> linear-Functional of (VectQuot a₂,(Ker a₃)) equals :: VECTSP10:def 13
QFunctional a₃,(Ker a₃);
correctness

proof end;

end;

:: deftheorem Def13 defines CQFunctional VECTSP10:def 13 :

theorem Th36: :: VECTSP10:36

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being VectSp of b₁
for b₃ being linear-Functional of b₂
for b₄ being Vector of (VectQuot b₂,(Ker b₃))
for b₅ being Vector of b₂ st b₄ = b₅ + (Ker b₃) holds
(CQFunctional b₃) . b₄ = b₃ . b₅

proof end;

registration

let c₁ be Field;
let c₂ be non trivial VectSp of c₁;
let c₃ be V71 linear-Functional of c₂;
cluster CQFunctional a₃ -> V71 0-preserving non trivial ;
coherence

proof end;

end;

registration

proof end;

end;