let A be non degenerated commutative Ring; :: thesis: for I being Ideal of A
for n being Nat st n > 0 holds
I ||^ (n + 1) = I *' (I ||^ n)
let I be Ideal of A; :: thesis: for n being Nat st n > 0 holds
I ||^ (n + 1) = I *' (I ||^ n)
let n be Nat; :: thesis: ( n > 0 implies I ||^ (n + 1) = I *' (I ||^ n) )
assume A1: n > 0 ; :: thesis: I ||^ (n + 1) = I *' (I ||^ n)
consider f being FinSequence of bool the carrier of A such that
A2: ( I ||^ (n + 1) = f . (len f) & len f = n + 1 & f . 1 = I ) and
A3: for i being Nat st i in dom f & i + 1 in dom f holds
f . (i + 1) = I *' (f /. i) by Def2;
consider g being FinSequence of bool the carrier of A such that
A4: ( I ||^ n = g . (len g) & len g = n & g . 1 = I ) and
A5: for i being Nat st i in dom g & i + 1 in dom g holds
g . (i + 1) = I *' (g /. i) by A1, Def2;
A6: ( len f > len g & len g > 0 ) by A1, A2, A4, XREAL_1:39;
A7: dom f = Seg (n + 1) by A2, FINSEQ_1:def 3;
A8: dom g = Seg n by A4, FINSEQ_1:def 3;
A9: 0 < 0 + n by A1;
A10: ( 1 <= n & n <= n + 1 ) by NAT_1:19, A9;
( 1 <= n + 1 & n + 1 <= n + 1 ) by NAT_1:12;
then A11: ( n in dom f & n + 1 in dom f ) by A7, A10;
( 1 <= n & n <= n ) by A9, NAT_1:19;
then A12: n in dom g by A8;
f /. n = f . n by A11, PARTFUN1:def 6
.= (f | (dom g)) . n by A12, FUNCT_1:49
.= I ||^ n by A4, A6, A2, A3, A5, Th9 ;
hence I ||^ (n + 1) = I *' (I ||^ n) by A2, A3, A11; :: thesis: verum