let R1, R2 be Relation of X; :: thesis: ( ex f being Function of X,NAT st
( R1 = value_of f & ( for x being Element of X st x in X holds
ex n being Nat st
( f . x = n & ( x . (iter (O,n)) <> {} or ( n = 0 & x . (iter (O,n)) = {} ) ) & x . (iter (O,(n + 1))) = {} ) ) ) & ex f being Function of X,NAT st
( R2 = value_of f & ( for x being Element of X st x in X holds
ex n being Nat st
( f . x = n & ( x . (iter (O,n)) <> {} or ( n = 0 & x . (iter (O,n)) = {} ) ) & x . (iter (O,(n + 1))) = {} ) ) ) implies R1 = R2 )
given f1 being Function of X,NAT such that A10: R1 = value_of f1 and
A11: for x being Element of X st x in X holds
ex n being Nat st
( f1 . x = n & ( x . (iter (O,n)) <> {} or ( n = 0 & x . (iter (O,n)) = {} ) ) & x . (iter (O,(n + 1))) = {} ) ; :: thesis: ( for f being Function of X,NAT holds
( not R2 = value_of f or ex x being Element of X st
( x in X & ( for n being Nat holds
( not f . x = n or ( not x . (iter (O,n)) <> {} & not ( n = 0 & x . (iter (O,n)) = {} ) ) or not x . (iter (O,(n + 1))) = {} ) ) ) ) or R1 = R2 )
given f2 being Function of X,NAT such that A12: R2 = value_of f2 and
A13: for x being Element of X st x in X holds
ex n being Nat st
( f2 . x = n & ( x . (iter (O,n)) <> {} or ( n = 0 & x . (iter (O,n)) = {} ) ) & x . (iter (O,(n + 1))) = {} ) ; :: thesis: R1 = R2
A14: ( dom f1 = X & dom f2 = X ) by FUNCT_2:def 1;
now :: thesis: for y being object st y in X holds
f1 . y = f2 . y
let y be object ; :: thesis: ( y in X implies f1 . y = f2 . y )
assume A15: y in X ; :: thesis: f1 . y = f2 . y
then reconsider x = y as Element of X ;
consider n1 being Nat such that
A16: ( f1 . x = n1 & ( x . (iter (O,n1)) <> {} or ( n1 = 0 & x . (iter (O,n1)) = {} ) ) & x . (iter (O,(n1 + 1))) = {} ) by A15, A11;
consider n2 being Nat such that
A17: ( f2 . x = n2 & ( x . (iter (O,n2)) <> {} or ( n2 = 0 & x . (iter (O,n2)) = {} ) ) & x . (iter (O,(n2 + 1))) = {} ) by A15, A13;
A18: now :: thesis: not n1 < n2
assume A19: n1 < n2 ; :: thesis: contradiction
then n1 + 1 <= n2 by NAT_1:13;
hence contradiction by A19, A16, A17, Th18, NAT_1:2; :: thesis: verum
end;
now :: thesis: not n2 < n1
assume A20: n2 < n1 ; :: thesis: contradiction
then n2 + 1 <= n1 by NAT_1:13;
hence contradiction by A20, A16, A17, Th18, NAT_1:2; :: thesis: verum
end;
hence f1 . y = f2 . y by A16, A17, A18, XXREAL_0:1; :: thesis: verum
end;
hence R1 = R2 by A10, A12, A14, FUNCT_1:2; :: thesis: verum