let T1, T2 be Function; :: thesis: ( dom T1 = NAT & T1 . 0 = x0 & ( for n being Nat holds
( T1 . n is pair & (T1 . (n + 1)) `1 = (L_ (T1 . n)) \/ (sqrt (x,(L_ (T1 . n)),(R_ (T1 . n)))) & (T1 . (n + 1)) `2 = ((R_ (T1 . n)) \/ (sqrt (x,(L_ (T1 . n)),(L_ (T1 . n))))) \/ (sqrt (x,(R_ (T1 . n)),(R_ (T1 . n)))) ) ) & dom T2 = NAT & T2 . 0 = x0 & ( for n being Nat holds
( T2 . n is pair & (T2 . (n + 1)) `1 = (L_ (T2 . n)) \/ (sqrt (x,(L_ (T2 . n)),(R_ (T2 . n)))) & (T2 . (n + 1)) `2 = ((R_ (T2 . n)) \/ (sqrt (x,(L_ (T2 . n)),(L_ (T2 . n))))) \/ (sqrt (x,(R_ (T2 . n)),(R_ (T2 . n)))) ) ) implies T1 = T2 )
assume that
A2: ( dom T1 = omega & T1 . 0 = x0 ) and
A3: for k being Nat holds
( T1 . k is pair & (T1 . (k + 1)) `1 = (L_ (T1 . k)) \/ (sqrt (x,(L_ (T1 . k)),(R_ (T1 . k)))) & (T1 . (k + 1)) `2 = ((R_ (T1 . k)) \/ (sqrt (x,(L_ (T1 . k)),(L_ (T1 . k))))) \/ (sqrt (x,(R_ (T1 . k)),(R_ (T1 . k)))) ) and
A4: ( dom T2 = omega & T2 . 0 = x0 ) and
A5: for k being Nat holds
( T2 . k is pair & (T2 . (k + 1)) `1 = (L_ (T2 . k)) \/ (sqrt (x,(L_ (T2 . k)),(R_ (T2 . k)))) & (T2 . (k + 1)) `2 = ((R_ (T2 . k)) \/ (sqrt (x,(L_ (T2 . k)),(L_ (T2 . k))))) \/ (sqrt (x,(R_ (T2 . k)),(R_ (T2 . k)))) ) ; :: thesis: T1 = T2
defpred S₁[ Nat] means T1 . $1 = T2 . $1;
A6: S₁[ 0 ] by A2, A4;
A7: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A8: S₁[n] ; :: thesis: S₁[n + 1]
A9: ( T1 . (n + 1) is pair & T2 . (n + 1) is pair ) by A3, A5;
R_ (T1 . (n + 1)) = ((R_ (T1 . n)) \/ (sqrt (x,(L_ (T1 . n)),(L_ (T1 . n))))) \/ (sqrt (x,(R_ (T1 . n)),(R_ (T1 . n)))) by A3;
then A10: (T1 . (n + 1)) `2 = R_ (T2 . (n + 1)) by A5, A8;
L_ (T1 . (n + 1)) = (L_ (T1 . n)) \/ (sqrt (x,(L_ (T1 . n)),(R_ (T1 . n)))) by A3;
then (T1 . (n + 1)) `1 = (T2 . (n + 1)) `1 by A5, A8;
hence S₁[n + 1] by A9, A10, XTUPLE_0:2; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A6, A7);
then for o being object st o in dom T1 holds
T1 . o = T2 . o by A2;
hence T1 = T2 by A2, A4, FUNCT_1:2; :: thesis: verum