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) )
A1: len (b * p) = len p by MATRIXR1:16;
A2: p is Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
assume A3: p is first-line-of-anti-circular ; :: thesis: (a * (ACirc p)) + (b * (ACirc p)) = ACirc ((a + b) * p)
then A4: ( a * p is first-line-of-anti-circular & b * p is first-line-of-anti-circular ) by Th62;
(a * (ACirc p)) + (b * (ACirc p)) = (ACirc (a * p)) + (b * (ACirc p)) by A3, Th63
.= (ACirc (a * p)) + (ACirc (b * p)) by A3, Th63
.= ACirc ((a * p) + (b * p)) by A4, A1, Th61, MATRIXR1:16 ;
hence (a * (ACirc p)) + (b * (ACirc p)) = ACirc ((a + b) * p) by A2, FVSUM_1:55; :: thesis: verum