let f be U-continuous Function; ( 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
; for a, y being set st [a,y] in Trace f holds
a is finite
let a, y be set ; ( [a,y] in Trace f implies a is finite )
assume A2:
[a,y] in Trace f
; a is finite
then A3:
a in dom f
by Th31;
y in f . a
by A2, Th31;
then consider b being set such that
A4:
b is finite
and
A5:
b c= a
and
A6:
y in f . b
by A1, A3, Th21;
b in dom f
by A1, A3, A5;
hence
a is finite
by A2, A4, A5, A6, Th31; verum