let A, B be set ; :: thesis: for R being Subset of [:A,B:] holds union ((.: R) .: A) c= R .: (union A)
let R be Subset of [:A,B:]; :: thesis: union ((.: R) .: A) c= R .: (union A)
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in union ((.: R) .: A) or y in R .: (union A) )
assume y in union ((.: R) .: A) ; :: thesis: 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 set such that
A3: X in dom (.: R) and
A4: X in A and
A5: Z = (.: R) . X by A2, FUNCT_1:def 12;
y in R .: X by A1, A3, A5, Th19;
then consider x being set such that
A6: ( [x,y] in R & x in X ) by RELAT_1:def 13;
x in union A by A4, A6, TARSKI:def 4;
hence y in R .: (union A) by A6, RELAT_1:def 13; :: thesis: verum