:: MATRLIN semantic presentation

definition

let c₁, c₂ be set ;
let c₃ be FinSequence-DOMAIN of c₁;
let c₄ be PartFunc of c₂,c₃;
let c₅ be set ;
redefine func /. as c₄ /. c₅ -> Element of a₃;
coherence ;

end;

theorem Th1: :: MATRLIN:1

canceled;

theorem Th2: :: MATRLIN:2

canceled;

definition

let c₁ be non empty set ;
let c₂ be Nat;
let c₃ be Matrix of c₁;
redefine func Del as Del c₃,c₂ -> Matrix of a₁;
coherence

proof end;

end;

theorem Th3: :: MATRLIN:3

for b₁ being Nat
for b₂ being FinSequence st len b₂ = b₁ + 1 holds
len (Del b₂,(b₁ + 1)) = b₁

proof end;

theorem Th4: :: MATRLIN:4

for b₁, b₂ being Nat
for b₃ being non empty set
for b₄ being Matrix of b₁ + 1,b₂,b₃
for b₅ being Matrix of b₃ holds
( ( b₁ > 0 implies width b₄ = width (Del b₄,(b₁ + 1)) ) & ( b₅ = <*(b₄ . (b₁ + 1))*> implies width b₄ = width b₅ ) )

proof end;

theorem Th5: :: MATRLIN:5

for b₁, b₂ being Nat
for b₃ being non empty set
for b₄ being Matrix of b₁ + 1,b₂,b₃ holds Del b₄,(b₁ + 1) is Matrix of b₁,b₂,b₃

proof end;

theorem Th6: :: MATRLIN:6

for b₁ being Nat
for b₂ being FinSequence st len b₂ = b₁ + 1 holds
b₂ = (Del b₂,(len b₂)) ^ <*(b₂ . (len b₂))*>

proof end;

definition

let c₁ be non empty set ;
let c₂ be FinSequence of c₁;
redefine func <* as <*c₂*> -> Matrix of 1, len a₂,a₁;
coherence by MATRIX_1:11;

end;

theorem Th7: :: MATRLIN:7

for b₁ being set
for b₂ being FinSequence holds (Sgm (b₂ " b₁)) ^ (Sgm (b₂ " ((rng b₂) \ b₁))) is Permutation of dom b₂

proof end;

theorem Th8: :: MATRLIN:8

for b₁ being FinSequence
for b₂ being Subset of (rng b₁) st b₁ is one-to-one holds
ex b₃ being Permutation of dom b₁ st (b₁ - (b₂ ` )) ^ (b₁ - b₂) = b₁ * b₃

proof end;

definition

let c₁ be Function;
attr a₁ is FinSequence-yielding means :Def1: :: MATRLIN:def 1
for b₁ being set st b₁ in dom a₁ holds
a₁ . b₁ is FinSequence;

end;

:: deftheorem Def1 defines FinSequence-yielding MATRLIN:def 1 :

registration

cluster FinSequence-yielding set ;
existence

proof end;

end;

definition

let c₁, c₂ be FinSequence-yielding Function;
func c₁ ^^ c₂ -> FinSequence-yielding Function means :Def2: :: MATRLIN:def 2
( dom a₃ = (dom a₁) /\ (dom a₂) & ( for b₁ being set st b₁ in dom a₃ holds
for b₂, b₃ being FinSequence st b₂ = a₁ . b₁ & b₃ = a₂ . b₁ holds
a₃ . b₁ = b₂ ^ b₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines ^^ MATRLIN:def 2 :

theorem Th9: :: MATRLIN:9

for b₁ being Field
for b₂ being VectSp of b₁
for b₃, b₄ being Linear_Combination of b₂
for b₅ being Subset of b₂ st b₅ is linearly-independent & Carrier b₃ c= b₅ & Carrier b₄ c= b₅ & Sum b₃ = Sum b₄ holds
b₃ = b₄

proof end;

theorem Th10: :: MATRLIN:10

for b₁ being Field
for b₂ being VectSp of b₁
for b₃, b₄, b₅ being Linear_Combination of b₂
for b₆ being Subset of b₂ st b₆ is linearly-independent & Carrier b₃ c= b₆ & Carrier b₄ c= b₆ & Carrier b₅ c= b₆ & Sum b₃ = (Sum b₄) + (Sum b₅) holds
b₃ = b₄ + b₅

proof end;

theorem Th11: :: MATRLIN:11

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Element of b₁
for b₄, b₅ being Linear_Combination of b₂
for b₆ being Subset of b₂ st b₆ is linearly-independent & Carrier b₄ c= b₆ & Carrier b₅ c= b₆ & b₃ <> 0. b₁ & Sum b₄ = b₃ * (Sum b₅) holds
b₄ = b₃ * b₅

proof end;

theorem Th12: :: MATRLIN:12

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Element of b₂
for b₄ being Basis of b₂ ex b₅ being Linear_Combination of b₂ st
( b₃ = Sum b₅ & Carrier b₅ c= b₄ )

proof end;

definition

let c₁ be Field;
let c₂ be VectSp of c₁;
attr a₂ is finite-dimensional means :Def3: :: MATRLIN:def 3
ex b₁ being finite Subset of a₂ st b₁ is Basis of a₂;

end;

:: deftheorem Def3 defines finite-dimensional MATRLIN:def 3 :

registration

let c₁ be Field;
cluster strict finite-dimensional VectSpStr of a₁;
existence

proof end;

end;

definition

let c₁ be Field;
let c₂ be finite-dimensional VectSp of c₁;
mode OrdBasis of c₂ -> FinSequence of the carrier of a₂ means :Def4: :: MATRLIN:def 4
( a₃ is one-to-one & rng a₃ is Basis of a₂ );
existence

proof end;

end;

:: deftheorem Def4 defines OrdBasis MATRLIN:def 4 :

Lemma15: for b₁, b₂ being FinSequence st len b₁ = len b₂ & ( for b₃ being Nat st b₃ in dom b₁ holds
b₁ . b₃ = b₂ . b₃ ) holds
b₁ = b₂

proof end;

definition

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂, c₃ be VectSp of c₁;
let c₄, c₅ be Function of c₂,c₃;
func c₄ + c₅ -> Function of a₂,a₃ means :Def5: :: MATRLIN:def 5
for b₁ being Element of a₂ holds a₆ . b₁ = (a₄ . b₁) + (a₅ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines + MATRLIN:def 5 :

definition

let c₁ be Field;
let c₂, c₃ be finite-dimensional VectSp of c₁;
let c₄ be Function of c₂,c₃;
let c₅ be Element of c₁;
func c₅ * c₄ -> Function of a₂,a₃ means :Def6: :: MATRLIN:def 6
for b₁ being Element of a₂ holds a₆ . b₁ = a₅ * (a₄ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines * MATRLIN:def 6 :

theorem Th13: :: MATRLIN:13

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃ being Element of b₂
for b₄ being FinSequence of the carrier of b₂
for b₅ being FinSequence of the carrier of b₁ st len b₄ = len b₅ & ( for b₆ being Nat
for b₇ being Element of b₁ st b₆ in dom b₄ & b₇ = b₅ . b₆ holds
b₄ . b₆ = b₇ * b₃ ) holds
Sum b₄ = (Sum b₅) * b₃

proof end;

theorem Th14: :: MATRLIN:14

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃ being Element of b₂
for b₄ being FinSequence of the carrier of b₁
for b₅ being FinSequence of the carrier of b₂ st len b₄ = len b₅ & ( for b₆ being Nat st b₆ in dom b₄ holds
b₅ . b₆ = (b₄ /. b₆) * b₃ ) holds
Sum b₅ = (Sum b₄) * b₃

proof end;

theorem Th15: :: MATRLIN:15

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being FinSequence of the carrier of b₁ st ( for b₃ being Nat st b₃ in dom b₂ holds
b₂ /. b₃ = 0. b₁ ) holds
Sum b₂ = 0. b₁

proof end;

definition

let c₁ be Field;
let c₂ be finite-dimensional VectSp of c₁;
let c₃ be FinSequence of the carrier of c₁;
let c₄ be FinSequence of the carrier of c₂;
func lmlt c₃,c₄ -> FinSequence of the carrier of a₂ equals :: MATRLIN:def 7
the lmult of a₂ .: a₃,a₄;
coherence ;

end;

:: deftheorem Def7 defines lmlt MATRLIN:def 7 :

theorem Th16: :: MATRLIN:16

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃ being FinSequence of the carrier of b₂
for b₄ being FinSequence of the carrier of b₁ st dom b₄ = dom b₃ holds
dom (lmlt b₄,b₃) = dom b₄

proof end;

definition

let c₁ be non empty LoopStr ;
let c₂ be FinSequence of the carrier of c₁ * ;
func Sum c₂ -> FinSequence of the carrier of a₁ means :Def8: :: MATRLIN:def 8
( len a₃ = len a₂ & ( for b₁ being Nat st b₁ in dom a₃ holds
a₃ /. b₁ = Sum (a₂ /. b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines Sum MATRLIN:def 8 :

theorem Th17: :: MATRLIN:17

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃ being Matrix of the carrier of b₂ st len b₃ = 0 holds
Sum (Sum b₃) = 0. b₂

proof end;

theorem Th18: :: MATRLIN:18

for b₁ being Nat
for b₂ being Field
for b₃ being finite-dimensional VectSp of b₂
for b₄ being Matrix of b₁ + 1,0,the carrier of b₃ holds Sum (Sum b₄) = 0. b₃

proof end;

theorem Th19: :: MATRLIN:19

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃ being Element of b₂ holds <*<*b₃*>*> = <*<*b₃*>*> @

proof end;

theorem Th20: :: MATRLIN:20

for b₁ being Field
for b₂, b₃ being finite-dimensional VectSp of b₁
for b₄ being Function of b₃,b₂
for b₅ being FinSequence of the carrier of b₃ st b₄ is linear holds
b₄ . (Sum b₅) = Sum (b₄ * b₅)

proof end;

theorem Th21: :: MATRLIN:21

for b₁ being Field
for b₂, b₃ being finite-dimensional VectSp of b₁
for b₄ being Function of b₃,b₂
for b₅ being FinSequence of the carrier of b₁
for b₆ being FinSequence of the carrier of b₃ st len b₆ = len b₅ & b₄ is linear holds
b₄ * (lmlt b₅,b₆) = lmlt b₅,(b₄ * b₆)

proof end;

theorem Th22: :: MATRLIN:22

for b₁ being Field
for b₂, b₃ being finite-dimensional VectSp of b₁
for b₄ being Function of b₃,b₂
for b₅ being OrdBasis of b₃
for b₆ being FinSequence of the carrier of b₁ st len b₆ = len b₅ & b₄ is linear holds
b₄ . (Sum (lmlt b₆,b₅)) = Sum (lmlt b₆,(b₄ * b₅))

proof end;

theorem Th23: :: MATRLIN:23

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃, b₄ being FinSequence of the carrier of b₂
for b₅ being Linear_Combination of b₂
for b₆ being Permutation of dom b₃ st b₄ = b₃ * b₆ holds
b₅ (#) b₄ = (b₅ (#) b₃) * b₆

proof end;

theorem Th24: :: MATRLIN:24

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃ being FinSequence of the carrier of b₂
for b₄ being Linear_Combination of b₂ st b₃ is one-to-one & Carrier b₄ c= rng b₃ holds
Sum (b₄ (#) b₃) = Sum b₄

proof end;

theorem Th25: :: MATRLIN:25

for b₁ being Field
for b₂, b₃ being finite-dimensional VectSp of b₁
for b₄, b₅ being Function of b₃,b₂
for b₆ being set
for b₇ being FinSequence of the carrier of b₃ st rng b₇ c= b₆ & b₄ is linear & b₅ is linear & ( for b₈ being Element of b₃ st b₈ in b₆ holds
b₄ . b₈ = b₅ . b₈ ) holds
b₄ . (Sum b₇) = b₅ . (Sum b₇)

proof end;

theorem Th26: :: MATRLIN:26

for b₁ being Field
for b₂, b₃ being finite-dimensional VectSp of b₁
for b₄, b₅ being Function of b₃,b₂ st b₄ is linear & b₅ is linear holds
for b₆ being OrdBasis of b₃ st len b₆ > 0 & b₄ * b₆ = b₅ * b₆ holds
b₄ = b₅

proof end;

registration

let c₁ be non empty set ;
cluster -> FinSequence-yielding FinSequence of a₁ * ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂, c₃ be Matrix of c₁;
redefine func ^^ as c₂ ^^ c₃ -> Matrix of a₁;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂, c₃, c₄ be Nat;
let c₅ be Matrix of c₂,c₄,c₁;
let c₆ be Matrix of c₃,c₄,c₁;
redefine func ^ as c₅ ^ c₆ -> Matrix of a₂ + a₃,a₄,a₁;
coherence

proof end;

end;

theorem Th27: :: MATRLIN:27

for b₁, b₂, b₃, b₄ being Nat
for b₅ being non empty set
for b₆ being Matrix of b₁,b₂,b₅
for b₇ being Matrix of b₃,b₂,b₅ st b₄ in dom b₆ holds
Line (b₆ ^ b₇),b₄ = Line b₆,b₄

proof end;

theorem Th28: :: MATRLIN:28

for b₁, b₂, b₃ being Nat
for b₄ being non empty set
for b₅ being Matrix of b₁,b₂,b₄
for b₆ being Matrix of b₃,b₂,b₄ st width b₅ = width b₆ holds
width (b₅ ^ b₆) = width b₅

proof end;

theorem Th29: :: MATRLIN:29

for b₁, b₂, b₃, b₄, b₅ being Nat
for b₆ being non empty set
for b₇ being Matrix of b₁,b₂,b₆
for b₈ being Matrix of b₃,b₂,b₆ st b₄ in dom b₈ & b₅ = (len b₇) + b₄ holds
Line (b₇ ^ b₈),b₅ = Line b₈,b₄

proof end;

theorem Th30: :: MATRLIN:30

for b₁, b₂, b₃ being Nat
for b₄ being non empty set
for b₅ being Matrix of b₁,b₂,b₄
for b₆ being Matrix of b₃,b₂,b₄ st width b₅ = width b₆ holds
for b₇ being Nat st b₇ in Seg (width b₅) holds
Col (b₅ ^ b₆),b₇ = (Col b₅,b₇) ^ (Col b₆,b₇)

proof end;

theorem Th31: :: MATRLIN:31

for b₁, b₂, b₃ being Nat
for b₄ being Field
for b₅ being VectSp of b₄
for b₆ being Matrix of b₁,b₂,the carrier of b₅
for b₇ being Matrix of b₃,b₂,the carrier of b₅ holds Sum (b₆ ^ b₇) = (Sum b₆) ^ (Sum b₇)

proof end;

theorem Th32: :: MATRLIN:32

for b₁, b₂, b₃ being Nat
for b₄ being non empty set
for b₅ being Matrix of b₁,b₂,b₄
for b₆ being Matrix of b₃,b₂,b₄ st width b₅ = width b₆ holds
(b₅ ^ b₆) @ = (b₅ @ ) ^^ (b₆ @ )

proof end;

theorem Th33: :: MATRLIN:33

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃, b₄ being Matrix of the carrier of b₂ holds the add of b₂ .: (Sum b₃),(Sum b₄) = Sum (b₃ ^^ b₄)

proof end;

definition

let c₁ be non empty set ;
let c₂ be BinOp of c₁;
let c₃, c₄ be FinSequence of c₁;
redefine func .: as c₂ .: c₃,c₄ -> FinSequence of a₁;
coherence

proof end;

end;

theorem Th34: :: MATRLIN:34

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃, b₄ being FinSequence of the carrier of b₂ st len b₃ = len b₄ holds
Sum (the add of b₂ .: b₃,b₄) = (Sum b₃) + (Sum b₄)

proof end;

theorem Th35: :: MATRLIN:35

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃, b₄ being Matrix of the carrier of b₂ st len b₃ = len b₄ holds
(Sum (Sum b₃)) + (Sum (Sum b₄)) = Sum (Sum (b₃ ^^ b₄))

proof end;

theorem Th36: :: MATRLIN:36

canceled;

theorem Th37: :: MATRLIN:37

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃ being Matrix of the carrier of b₂ holds Sum (Sum b₃) = Sum (Sum (b₃ @ ))

proof end;

theorem Th38: :: MATRLIN:38

for b₁, b₂ being Nat
for b₃ being Field
for b₄ being finite-dimensional VectSp of b₃
for b₅ being Matrix of b₁,b₂,the carrier of b₃ st b₁ > 0 & b₂ > 0 holds
for b₆, b₇ being FinSequence of the carrier of b₃ st len b₆ = b₁ & len b₇ = b₂ & ( for b₈ being Nat st b₈ in dom b₇ holds
b₇ /. b₈ = Sum (mlt b₆,(Col b₅,b₈)) ) holds
for b₈, b₉ being FinSequence of the carrier of b₄ st len b₈ = b₂ & len b₉ = b₁ & ( for b₁₀ being Nat st b₁₀ in dom b₉ holds
b₉ /. b₁₀ = Sum (lmlt (Line b₅,b₁₀),b₈) ) holds
Sum (lmlt b₆,b₉) = Sum (lmlt b₇,b₈)

proof end;

definition

let c₁ be Field;
let c₂ be finite-dimensional VectSp of c₁;
let c₃ be OrdBasis of c₂;
let c₄ be Element of c₂;
func c₄ |-- c₃ -> FinSequence of the carrier of a₁ means :Def9: :: MATRLIN:def 9
( len a₅ = len a₃ & ex b₁ being Linear_Combination of a₂ st
( a₄ = Sum b₁ & Carrier b₁ c= rng a₃ & ( for b₂ being Nat st 1 <= b₂ & b₂ <= len a₅ holds
a₅ /. b₂ = b₁ . (a₃ /. b₂) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines |-- MATRLIN:def 9 :

Lemma43: for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃ being OrdBasis of b₂
for b₄ being Element of b₂ holds dom (b₄ |-- b₃) = dom b₃

proof end;

theorem Th39: :: MATRLIN:39

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃ being OrdBasis of b₂
for b₄, b₅ being Vector of b₂ st b₄ |-- b₃ = b₅ |-- b₃ holds
b₄ = b₅

proof end;

theorem Th40: :: MATRLIN:40

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃ being OrdBasis of b₂
for b₄ being Element of b₂ holds b₄ = Sum (lmlt (b₄ |-- b₃),b₃)

proof end;

theorem Th41: :: MATRLIN:41

for b₁ being Field
for b₂ being finite-dimensional VectSp of b₁
for b₃ being OrdBasis of b₂
for b₄ being FinSequence of the carrier of b₁ st len b₄ = len b₃ holds
b₄ = (Sum (lmlt b₄,b₃)) |-- b₃

proof end;

Lemma47: for b₁ being FinSequence
for b₂ being set st b₂ in dom b₁ holds
len b₁ > 0

proof end;

theorem Th42: :: MATRLIN:42

for b₁ being Field
for b₂, b₃ being finite-dimensional VectSp of b₁
for b₄ being Function of b₂,b₃
for b₅ being OrdBasis of b₂
for b₆ being OrdBasis of b₃
for b₇, b₈ being FinSequence of the carrier of b₁ st len b₇ = len b₅ holds
for b₉ being Nat st b₉ in dom b₆ & len b₈ = len b₅ & ( for b₁₀ being Nat st b₁₀ in dom b₅ holds
b₈ . b₁₀ = ((b₄ . (b₅ /. b₁₀)) |-- b₆) /. b₉ ) & len b₅ > 0 holds
((Sum (lmlt b₇,(b₄ * b₅))) |-- b₆) /. b₉ = Sum (mlt b₇,b₈)

proof end;

definition

let c₁ be Field;
let c₂, c₃ be finite-dimensional VectSp of c₁;
let c₄ be Function of the carrier of c₂,the carrier of c₃;
let c₅ be FinSequence of the carrier of c₂;
let c₆ be OrdBasis of c₃;
func AutMt c₄,c₅,c₆ -> Matrix of a₁ means :Def10: :: MATRLIN:def 10
( len a₇ = len a₅ & ( for b₁ being Nat st b₁ in dom a₅ holds
a₇ /. b₁ = (a₄ . (a₅ /. b₁)) |-- a₆ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines AutMt MATRLIN:def 10 :

Lemma50: for b₁ being Field
for b₂, b₃ being finite-dimensional VectSp of b₁
for b₄ being Function of b₂,b₃
for b₅ being OrdBasis of b₂
for b₆ being OrdBasis of b₃ holds dom (AutMt b₄,b₅,b₆) = dom b₅

proof end;

theorem Th43: :: MATRLIN:43

for b₁ being Field
for b₂, b₃ being finite-dimensional VectSp of b₁
for b₄ being Function of b₂,b₃
for b₅ being OrdBasis of b₂
for b₆ being OrdBasis of b₃ st len b₅ = 0 holds
AutMt b₄,b₅,b₆ = {}

proof end;

theorem Th44: :: MATRLIN:44

for b₁ being Field
for b₂, b₃ being finite-dimensional VectSp of b₁
for b₄ being Function of b₂,b₃
for b₅ being OrdBasis of b₂
for b₆ being OrdBasis of b₃ st len b₅ > 0 holds
width (AutMt b₄,b₅,b₆) = len b₆

proof end;

theorem Th45: :: MATRLIN:45

for b₁ being Field
for b₂, b₃ being finite-dimensional VectSp of b₁
for b₄, b₅ being Function of b₂,b₃
for b₆ being OrdBasis of b₂
for b₇ being OrdBasis of b₃ st b₄ is linear & b₅ is linear & AutMt b₄,b₆,b₇ = AutMt b₅,b₆,b₇ & len b₆ > 0 holds
b₄ = b₅

proof end;

theorem Th46: :: MATRLIN:46

for b₁ being Field
for b₂, b₃, b₄ being finite-dimensional VectSp of b₁
for b₅ being Function of b₂,b₃
for b₆ being Function of b₃,b₄
for b₇ being OrdBasis of b₂
for b₈ being OrdBasis of b₃
for b₉ being OrdBasis of b₄ st b₅ is linear & b₆ is linear & len b₇ > 0 & len b₈ > 0 & len b₉ > 0 holds
AutMt (b₆ * b₅),b₇,b₉ = (AutMt b₅,b₇,b₈) * (AutMt b₆,b₈,b₉)

proof end;

theorem Th47: :: MATRLIN:47

for b₁ being Field
for b₂, b₃ being finite-dimensional VectSp of b₁
for b₄, b₅ being Function of b₂,b₃
for b₆ being OrdBasis of b₂
for b₇ being OrdBasis of b₃ holds AutMt (b₄ + b₅),b₆,b₇ = (AutMt b₄,b₆,b₇) + (AutMt b₅,b₆,b₇)

proof end;

theorem Th48: :: MATRLIN:48

for b₁ being Field
for b₂ being Element of b₁
for b₃, b₄ being finite-dimensional VectSp of b₁
for b₅ being Function of b₃,b₄
for b₆ being OrdBasis of b₃
for b₇ being OrdBasis of b₄ st b₂ <> 0. b₁ holds
AutMt (b₂ * b₅),b₆,b₇ = b₂ * (AutMt b₅,b₆,b₇)

proof end;