let n be Nat; :: thesis: for x, y1, y2 being Element of NAT * st S₂[n,x,y1] & S₂[n,x,y2] holds
y1 = y2
let x, y1, y2 be Element of NAT * ; :: thesis: ( S₂[n,x,y1] & S₂[n,x,y2] implies y1 = y2 )
assume A1: ( ( for k being Element of NAT st n + 2 = 2 * k holds
y1 = x ^ <*(x /. k)*> ) & ( for k being Element of NAT st n + 2 = (2 * k) + 1 holds
y1 = x ^ <*((x /. k) + (x /. (k + 1)))*> ) ) ; :: thesis: ( not S₂[n,x,y2] or y1 = y2 )
n + 2 = (2 * ((n + 2) div 2)) + ((n + 2) mod 2) by NAT_D:2;
then A2: ( n + 2 = (2 * ((n + 2) div 2)) + 0 or n + 2 = (2 * ((n + 2) div 2)) + 1 ) by NAT_D:12;
assume ( ( for k being Element of NAT st n + 2 = 2 * k holds
y2 = x ^ <*(x /. k)*> ) & ( for k being Element of NAT st n + 2 = (2 * k) + 1 holds
y2 = x ^ <*((x /. k) + (x /. (k + 1)))*> ) ) ; :: thesis: y1 = y2
then ( ( y1 = x ^ <*(x /. ((n + 2) div 2))*> & y2 = x ^ <*(x /. ((n + 2) div 2))*> ) or ( y1 = x ^ <*((x /. ((n + 2) div 2)) + (x /. (((n + 2) div 2) + 1)))*> & y2 = x ^ <*((x /. ((n + 2) div 2)) + (x /. (((n + 2) div 2) + 1)))*> ) ) by A1, A2;
hence y1 = y2 ; :: thesis: verum