let P be FinSequence-membered set ; :: thesis: ( P ^^ 0 = {{}} & ( for n being Nat holds P ^^ (n + 1) = (P ^^ n) ^ P ) )
thus P ^^ 0 = {{}} by Def3; :: thesis: for n being Nat holds P ^^ (n + 1) = (P ^^ n) ^ P
let n be Nat; :: thesis: P ^^ (n + 1) = (P ^^ n) ^ P
consider Q being FinSequence-membered set such that
A1: ( Q = P ^^ n & P ^^ (n + 1) = Q ^ P ) by Def3;
thus P ^^ (n + 1) = (P ^^ n) ^ P by A1; :: thesis: verum