let n be Nat; :: thesis: for x being Element of NAT * ex y being Element of NAT * st S₁[n,x,y]
let x be Element of NAT * ; :: thesis: ex y being Element of NAT * st S₁[n,x,y]
( (n + 2) mod 2 = 0 or (n + 2) mod 2 <> 0 ) ;
then consider y being FinSequence of NAT such that
A1: ( ( (n + 2) mod 2 = 0 & y = x ^ <*(x /. ((n + 2) div 2))*> ) or ( (n + 2) mod 2 <> 0 & y = x ^ <*((x /. ((n + 2) div 2)) + (x /. (((n + 2) div 2) + 1)))*> ) ) ;
reconsider y = y as Element of NAT * by FINSEQ_1:def 11;
take y ; :: thesis: S₁[n,x,y]

hereby :: thesis: for k being Nat st n + 2 = (2 * k) + 1 holds
y = x ^ <*((x /. k) + (x /. (k + 1)))*>

let k be Nat; :: thesis: ( n + 2 = 2 * k implies y = x ^ <*(x /. k)*> )
assume n + 2 = 2 * k ; :: thesis: y = x ^ <*(x /. k)*>
then n + 2 = (2 * k) + 0 ;
hence y = x ^ <*(x /. k)*> by A1, NAT_D:def 1, NAT_D:def 2; :: thesis: verum

end;

hereby :: thesis: verum

let k be Nat; :: thesis: ( n + 2 = (2 * k) + 1 implies y = x ^ <*((x /. k) + (x /. (k + 1)))*> )
assume A2: n + 2 = (2 * k) + 1 ; :: thesis: y = x ^ <*((x /. k) + (x /. (k + 1)))*>
then (n + 2) div 2 = k by NAT_D:def 1;
hence y = x ^ <*((x /. k) + (x /. (k + 1)))*> by A1, A2, NAT_D:def 2; :: thesis: verum

end;