let A be set ; for f being Function st A c= bool (dom f) holds
f .: (union A) = union ((.: f) .: A)
let f be Function; ( A c= bool (dom f) implies f .: (union A) = union ((.: f) .: A) )
assume A1:
A c= bool (dom f)
; f .: (union A) = union ((.: f) .: A)
A2:
f .: (union A) c= union ((.: f) .: A)
proof
let y be
set ;
TARSKI:def 3 ( not y in f .: (union A) or y in union ((.: f) .: A) )
assume
y in f .: (union A)
;
y in union ((.: f) .: A)
then consider x being
set such that
x in dom f
and A3:
x in union A
and A4:
y = f . x
by FUNCT_1:def 6;
consider X being
set such that A5:
x in X
and A6:
X in A
by A3, TARSKI:def 4;
X in bool (dom f)
by A1, A6;
then
X in dom (.: f)
by Def1;
then A7:
(.: f) . X in (.: f) .: A
by A6, FUNCT_1:def 6;
y in f .: X
by A1, A4, A5, A6, FUNCT_1:def 6;
then
y in (.: f) . X
by A1, A6, Def1;
hence
y in union ((.: f) .: A)
by A7, TARSKI:def 4;
verum
end;
union ((.: f) .: A) c= f .: (union A)
by Th15;
hence
f .: (union A) = union ((.: f) .: A)
by A2, XBOOLE_0:def 10; verum