let A be finite Ordinal-Sequence; :: thesis: for b being Ordinal
for n being Nat holds b -leading_coeff (A /^ n) = (b -leading_coeff A) /^ n
let b be Ordinal; :: thesis: for n being Nat holds b -leading_coeff (A /^ n) = (b -leading_coeff A) /^ n
let n be Nat; :: thesis: b -leading_coeff (A /^ n) = (b -leading_coeff A) /^ n
A1: dom (b -leading_coeff (A /^ n)) = len (A /^ n) by Def3
.= (len A) -' n by AFINSQ_2:def 2
.= (len (b -leading_coeff A)) -' n by Def3
.= dom ((b -leading_coeff A) /^ n) by AFINSQ_2:def 2 ;

now :: thesis: for k being Nat st k in dom (b -leading_coeff (A /^ n)) holds
(b -leading_coeff (A /^ n)) . k = ((b -leading_coeff A) /^ n) . k

let k be Nat; :: thesis: ( k in dom (b -leading_coeff (A /^ n)) implies (b -leading_coeff (A /^ n)) . k = ((b -leading_coeff A) /^ n) . k )
assume A2: k in dom (b -leading_coeff (A /^ n)) ; :: thesis: (b -leading_coeff (A /^ n)) . k = ((b -leading_coeff A) /^ n) . k
then A3: k in dom (A /^ n) by Def3;
A4: b -leading_coeff (A . (k + n)) = (b -leading_coeff A) . (k + n)

proof

per cases ( k + n in dom A or not k + n in dom A ) ;

suppose k + n in dom A ; :: thesis: b -leading_coeff (A . (k + n)) = (b -leading_coeff A) . (k + n)

hence b -leading_coeff (A . (k + n)) = (b -leading_coeff A) . (k + n) by Def3; :: thesis: verum

end;

suppose A5: not k + n in dom A ; :: thesis: b -leading_coeff (A . (k + n)) = (b -leading_coeff A) . (k + n)

then A . (k + n) = {} by FUNCT_1:def 2;
then A6: b -leading_coeff (A . (k + n)) = {} by ORDINAL3:70;
not k + n in dom (b -leading_coeff A) by A5, Def3;
hence b -leading_coeff (A . (k + n)) = (b -leading_coeff A) . (k + n) by A6, FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

thus (b -leading_coeff (A /^ n)) . k = b -leading_coeff ((A /^ n) . k) by A3, Def3
.= b -leading_coeff (A . (k + n)) by A3, AFINSQ_2:def 2
.= ((b -leading_coeff A) /^ n) . k by A1, A2, A4, AFINSQ_2:def 2 ; :: thesis: verum

end;

hence b -leading_coeff (A /^ n) = (b -leading_coeff A) /^ n by A1, AFINSQ_1:8; :: thesis: verum