let s be Nat; :: thesis: ex f being increasing fAP-like positive-yielding FinSequence of NAT st
( len f = s & ( for i being Nat st 1 <= i & i <= len f holds
f . i is perfect_power ) )

per cases ( s = 0 or s <> 0 ) ;

suppose A1: s = 0 ; :: thesis: ex f being increasing fAP-like positive-yielding FinSequence of NAT st
( len f = s & ( for i being Nat st 1 <= i & i <= len f holds
f . i is perfect_power ) )

take <*> NAT ; :: thesis: ( len (<*> NAT) = s & ( for i being Nat st 1 <= i & i <= len (<*> NAT) holds
(<*> NAT) . i is perfect_power ) )
thus ( len (<*> NAT) = s & ( for i being Nat st 1 <= i & i <= len (<*> NAT) holds
(<*> NAT) . i is perfect_power ) ) by A1; :: thesis: verum

end;

suppose s <> 0 ; :: thesis: ex f being increasing fAP-like positive-yielding FinSequence of NAT st
( len f = s & ( for i being Nat st 1 <= i & i <= len f holds
f . i is perfect_power ) )

then reconsider s1 = s as non zero Nat ;
take f = Problem58Solution s1; :: thesis: ( len f = s & ( for i being Nat st 1 <= i & i <= len f holds
f . i is perfect_power ) )
thus A2: len f = s by CARD_1:def 7; :: thesis: for i being Nat st 1 <= i & i <= len f holds
f . i is perfect_power
let k be Nat; :: thesis: ( 1 <= k & k <= len f implies f . k is perfect_power )
assume that
A3: 1 <= k and
A4: k <= len f ; :: thesis: f . k is perfect_power
reconsider k = k as non zero Nat by A3;
take (sequenceQk s) . k ; :: according to NUMBER06:def 10 :: thesis: ex b₁ being set st
( not b₁ <= 1 & f . k = ((sequenceQk s) . k) |^ b₁ )
take primenumber (k - 1) ; :: thesis: ( not primenumber (k - 1) <= 1 & f . k = ((sequenceQk s) . k) |^ (primenumber (k - 1)) )
thus primenumber (k - 1) > 1 by INT_2:def 4; :: thesis: f . k = ((sequenceQk s) . k) |^ (primenumber (k - 1))
thus f . k = ((sequenceQk s) . k) |^ (primenumber (k - 1)) by A2, A4, Th50; :: thesis: verum

end;

end;