let n be Nat; :: thesis: for s being positive Nat
for f being b₁ -element natural-valued positive FinSequence st f is with_sum_of_squares_of_reciprocals_equal_1 holds
ex g being b₁ + (3 * n) -element natural-valued positive FinSequence st g is with_sum_of_squares_of_reciprocals_equal_1
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 * n) -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 * n) -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 * n) -element natural-valued positive FinSequence st g is with_sum_of_squares_of_reciprocals_equal_1
defpred S₁[ Nat] means ex g being s + (3 * $1) -element natural-valued positive FinSequence st g is with_sum_of_squares_of_reciprocals_equal_1 ;
A2: S₁[ 0 ] by A1;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume ex g being s + (3 * k) -element natural-valued positive FinSequence st g is with_sum_of_squares_of_reciprocals_equal_1 ; :: thesis: S₁[k + 1]
then ex h being (s + (3 * k)) + 3 -element natural-valued positive FinSequence st h is with_sum_of_squares_of_reciprocals_equal_1 by Lm28;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A3);
hence ex g being s + (3 * n) -element natural-valued positive FinSequence st g is with_sum_of_squares_of_reciprocals_equal_1 ; :: thesis: verum