let s be positive Nat; :: thesis: for f being s -element natural-valued positive FinSequence st f is with_sum_of_squares_of_reciprocals_equal_1 holds
ex g being s + 3 -element natural-valued positive FinSequence st g is with_sum_of_squares_of_reciprocals_equal_1
let f be s -element natural-valued positive FinSequence; :: thesis: ( f is with_sum_of_squares_of_reciprocals_equal_1 implies ex g being s + 3 -element natural-valued positive FinSequence st g is with_sum_of_squares_of_reciprocals_equal_1 )
set g = (f | (s - 1)) ^ <*(2 * (f . s)),(2 * (f . s)),(2 * (f . s)),(2 * (f . s))*>;
assume A1: f is with_sum_of_squares_of_reciprocals_equal_1 ; :: thesis: ex g being s + 3 -element natural-valued positive FinSequence st g is with_sum_of_squares_of_reciprocals_equal_1
reconsider g = (f | (s - 1)) ^ <*(2 * (f . s)),(2 * (f . s)),(2 * (f . s)),(2 * (f . s))*> as s + 3 -element natural-valued positive FinSequence ;
take g ; :: thesis: g is with_sum_of_squares_of_reciprocals_equal_1
thus g is with_sum_of_squares_of_reciprocals_equal_1 by A1, Th140; :: thesis: verum