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 object ; :: 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 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; :: thesis: verum