let P be FinSequence-membered set ; :: thesis: P ^^ 1 = P
thus P ^^ 1 = P ^^ (0 + 1)
.= (P ^^ 0) ^ P by Th6
.= {{}} ^ P by Th6
.= P by Th3 ; :: thesis: verum