now

let x be set ; :: thesis: ( x in dom f implies f . x is finite )
assume A1: x in dom f ; :: thesis: f . x is finite
then reconsider A = A as non empty set ;
reconsider x' = x as Element of A by A1;
reconsider f' = f as Function of A, Fin B ;
f' . x' is finite ;
hence f . x is finite ; :: thesis: verum

end;

hence Union f is finite by Th134; :: thesis: verum