now :: thesis: for x being object st x in dom f holds
f . x is finite

let x be object ; :: 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 x9 = x as Element of A by A1;
reconsider f9 = f as Function of A,(Fin B) ;
f9 . x9 is finite ;
hence f . x is finite ; :: thesis: verum

end;

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