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

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

let k be Nat; :: thesis: ( k in dom (b -exponent (A /^ n)) implies (b -exponent (A /^ n)) . k = ((b -exponent A) /^ n) . k )
assume A2: k in dom (b -exponent (A /^ n)) ; :: thesis: (b -exponent (A /^ n)) . k = ((b -exponent A) /^ n) . k
then A3: k in dom (A /^ n) by Def1;
A4: b -exponent (A . (k + n)) = (b -exponent 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 -exponent (A . (k + n)) = (b -exponent A) . (k + n)

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

end;

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

then A . (k + n) = {} by FUNCT_1:def 2;
then A6: b -exponent (A . (k + n)) = {} by ORDINAL5:def 10;
not k + n in dom (b -exponent A) by A5, Def1;
hence b -exponent (A . (k + n)) = (b -exponent A) . (k + n) by A6, FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

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

end;

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