let A be set ; for f being Function holds union ((.: f) .: A) c= f .: (union A)
let f be Function; union ((.: f) .: A) c= f .: (union A)
let y be object ; TARSKI:def 3 ( not y in union ((.: f) .: A) or y in f .: (union A) )
assume
y in union ((.: f) .: A)
; y in f .: (union A)
then consider Z being set such that
A1:
y in Z
and
A2:
Z in (.: f) .: A
by TARSKI:def 4;
consider X being object such that
A3:
X in dom (.: f)
and
A4:
X in A
and
A5:
Z = (.: f) . X
by A2, FUNCT_1:def 6;
reconsider X = X as set by TARSKI:1;
y in f .: X
by A1, A3, A5, Th7;
then consider x being object such that
A6:
x in dom f
and
A7:
x in X
and
A8:
y = f . x
by FUNCT_1:def 6;
x in union A
by A4, A7, TARSKI:def 4;
hence
y in f .: (union A)
by A6, A8, FUNCT_1:def 6; verum