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