let f be U-continuous Function; :: thesis: ( dom f is subset-closed implies for a, y being set st [a,y] in Trace f holds
a is finite )
assume A1: dom f is subset-closed ; :: thesis: for a, y being set st [a,y] in Trace f holds
a is finite
let a, y be set ; :: thesis: ( [a,y] in Trace f implies a is finite )
assume A2: [a,y] in Trace f ; :: thesis: a is finite
then A3: ( a in dom f & y in f . a & ( for b being set st b in dom f & b c= a & y in f . b holds
a = b ) ) by Th32;
then consider b being set such that
A4: ( b is finite & b c= a & y in f . b ) by A1, Th22;
b in dom f by A1, A3, A4, CLASSES1:def 1;
hence a is finite by A2, A4, Th32; :: thesis: verum