let A, B be set ; for R being Subset of [:A,B:] holds union ((.: R) .: A) c= R .: (union A)
let R be Subset of [:A,B:]; union ((.: R) .: A) c= R .: (union A)
let y be object ; TARSKI:def 3 ( not y in union ((.: R) .: A) or y in R .: (union A) )
assume
y in union ((.: R) .: A)
; y in R .: (union A)
then consider Z being set such that
A1:
y in Z
and
A2:
Z in (.: R) .: A
by TARSKI:def 4;
consider X being object such that
A3:
X in dom (.: R)
and
A4:
X in A
and
A5:
Z = (.: R) . X
by A2, FUNCT_1:def 6;
reconsider X = X as set by TARSKI:1;
y in R .: X
by A1, A3, A5, Th19;
then consider x being object such that
A6:
[x,y] in R
and
A7:
x in X
by RELAT_1:def 13;
x in union A
by A4, A7, TARSKI:def 4;
hence
y in R .: (union A)
by A6, RELAT_1:def 13; verum