let K be Field; :: thesis: for a, b being Element of K
for p, q being FinSequence of K st p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q holds
(a * (ACirc p)) + (b * (ACirc q)) = ACirc ((a * p) + (b * q))
let a, b be Element of K; :: thesis: for p, q being FinSequence of K st p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q holds
(a * (ACirc p)) + (b * (ACirc q)) = ACirc ((a * p) + (b * q))
let p, q be FinSequence of K; :: thesis: ( p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q implies (a * (ACirc p)) + (b * (ACirc q)) = ACirc ((a * p) + (b * q)) )
set n = len p;
assume A1: ( p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q ) ; :: thesis: (a * (ACirc p)) + (b * (ACirc q)) = ACirc ((a * p) + (b * q))
then A4: ( a * p is first-line-of-anti-circular & b * q is first-line-of-anti-circular ) by Th62;
A6: ( len (a * p) = len p & len (b * q) = len p ) by A1, MATRIXR1:16;
(a * (ACirc p)) + (b * (ACirc q)) = (ACirc (a * p)) + (b * (ACirc q)) by A1, Th63
.= (ACirc (a * p)) + (ACirc (b * q)) by A1, Th63
.= ACirc ((a * p) + (b * q)) by A4, A6, Th61 ;
hence (a * (ACirc p)) + (b * (ACirc q)) = ACirc ((a * p) + (b * q)) ; :: thesis: verum