let K be Field; :: thesis: for a, b being Element of K
for p being FinSequence of K st p is first-line-of-anti-circular holds
(a * (ACirc p)) + (b * (ACirc p)) = ACirc ((a + b) * p)
let a, b be Element of K; :: thesis: for p being FinSequence of K st p is first-line-of-anti-circular holds
(a * (ACirc p)) + (b * (ACirc p)) = ACirc ((a + b) * p)
let p be FinSequence of K; :: thesis: ( p is first-line-of-anti-circular implies (a * (ACirc p)) + (b * (ACirc p)) = ACirc ((a + b) * p) )
set n = len p;
assume A1: p is first-line-of-anti-circular ; :: thesis: (a * (ACirc p)) + (b * (ACirc p)) = ACirc ((a + b) * p)
A3: ( a * p is first-line-of-anti-circular & b * p is first-line-of-anti-circular ) by A1, Th62;
A4: ( len (a * p) = len p & len (b * p) = len p ) by MATRIXR1:16;
A5: (a * (ACirc p)) + (b * (ACirc p)) = (ACirc (a * p)) + (b * (ACirc p)) by A1, Th63
.= (ACirc (a * p)) + (ACirc (b * p)) by A1, Th63
.= ACirc ((a * p) + (b * p)) by A3, A4, Th61 ;
p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:110;
hence (a * (ACirc p)) + (b * (ACirc p)) = ACirc ((a + b) * p) by A5, FVSUM_1:68; :: thesis: verum