consider Q being FinSequence-membered set such that
A1: Q = (P ^^) . n and
(P ^^) . (n + 1) = Q ^ P by Def3;
thus (P ^^) . n is FinSequence-membered set by A1; :: thesis: verum