let K be Field; for a being Element of K
for p, q being FinSequence of K st p is first-line-of-circulant & q is first-line-of-circulant & len p = len q holds
(a * (LCirc p)) + (a * (LCirc q)) = LCirc (a * (p + q))
let a be Element of K; for p, q being FinSequence of K st p is first-line-of-circulant & q is first-line-of-circulant & len p = len q holds
(a * (LCirc p)) + (a * (LCirc q)) = LCirc (a * (p + q))
let p, q be FinSequence of K; ( p is first-line-of-circulant & q is first-line-of-circulant & len p = len q implies (a * (LCirc p)) + (a * (LCirc q)) = LCirc (a * (p + q)) )
assume that
A1:
( p is first-line-of-circulant & q is first-line-of-circulant )
and
A2:
len p = len q
; (a * (LCirc p)) + (a * (LCirc q)) = LCirc (a * (p + q))
A3:
( len (LCirc p) = len p & width (LCirc p) = len p )
by MATRIX_0:24;
( len (LCirc q) = len p & width (LCirc q) = len p )
by A2, MATRIX_0:24;
then (a * (LCirc p)) + (a * (LCirc q)) =
a * ((LCirc p) + (LCirc q))
by A3, MATRIX_5:20
.=
a * (LCirc (p + q))
by A1, A2, Th34
.=
LCirc (a * (p + q))
by A1, A2, Th33, Th42
;
hence
(a * (LCirc p)) + (a * (LCirc q)) = LCirc (a * (p + q))
; verum