let f be U-continuous Function; :: thesis: ( dom f is subset-closed implies for a being set st a in dom f holds
f . a = union (f .: (Fin a)) )
assume A1: dom f is subset-closed ; :: thesis: for a being set st a in dom f holds
f . a = union (f .: (Fin a))
let a be set ; :: thesis: ( a in dom f implies f . a = union (f .: (Fin a)) )
assume A2: a in dom f ; :: thesis: f . a = union (f .: (Fin a))
then reconsider C = dom f as non empty subset-closed d.union-closed set by A1;
reconsider a = a as Element of C by A2;
f . a = f . (union (Fin a)) by Th19;
hence f . a = union (f .: (Fin a)) by Def10; :: thesis: verum