let T1, T2 be Function; :: thesis: ( dom T1 = NAT & T1 . 0 = 1_No & ( for k being Nat holds
( T1 . k is pair & (T1 . (k + 1)) `1 = ((L_ (T1 . k)) \/ (divset ((L_ (T1 . k)),x,(R_ x),Inv))) \/ (divset ((R_ (T1 . k)),x,(L_ x),Inv)) & (T1 . (k + 1)) `2 = ((R_ (T1 . k)) \/ (divset ((L_ (T1 . k)),x,(L_ x),Inv))) \/ (divset ((R_ (T1 . k)),x,(R_ x),Inv)) ) ) & dom T2 = NAT & T2 . 0 = 1_No & ( for k being Nat holds
( T2 . k is pair & (T2 . (k + 1)) `1 = ((L_ (T2 . k)) \/ (divset ((L_ (T2 . k)),x,(R_ x),Inv))) \/ (divset ((R_ (T2 . k)),x,(L_ x),Inv)) & (T2 . (k + 1)) `2 = ((R_ (T2 . k)) \/ (divset ((L_ (T2 . k)),x,(L_ x),Inv))) \/ (divset ((R_ (T2 . k)),x,(R_ x),Inv)) ) ) implies T1 = T2 )
assume that
A2: ( dom T1 = omega & T1 . 0 = 1_No ) and
A3: for k being Nat holds
( T1 . k is pair & L_ (T1 . (k + 1)) = ((L_ (T1 . k)) \/ (divset ((L_ (T1 . k)),x,(R_ x),Inv))) \/ (divset ((R_ (T1 . k)),x,(L_ x),Inv)) & R_ (T1 . (k + 1)) = ((R_ (T1 . k)) \/ (divset ((L_ (T1 . k)),x,(L_ x),Inv))) \/ (divset ((R_ (T1 . k)),x,(R_ x),Inv)) ) and
A4: ( dom T2 = omega & T2 . 0 = 1_No ) and
A5: for k being Nat holds
( T2 . k is pair & L_ (T2 . (k + 1)) = ((L_ (T2 . k)) \/ (divset ((L_ (T2 . k)),x,(R_ x),Inv))) \/ (divset ((R_ (T2 . k)),x,(L_ x),Inv)) & R_ (T2 . (k + 1)) = ((R_ (T2 . k)) \/ (divset ((L_ (T2 . k)),x,(L_ x),Inv))) \/ (divset ((R_ (T2 . k)),x,(R_ x),Inv)) ) ; :: 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)) \/ (divset ((L_ (T1 . n)),x,(L_ x),Inv))) \/ (divset ((R_ (T1 . n)),x,(R_ x),Inv)) by A3;
then A10: (T1 . (n + 1)) `2 = R_ (T2 . (n + 1)) by A5, A8;
L_ (T1 . (n + 1)) = ((L_ (T1 . n)) \/ (divset ((L_ (T1 . n)),x,(R_ x),Inv))) \/ (divset ((R_ (T1 . n)),x,(L_ x),Inv)) 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