let X be non empty set ; :: thesis: for D being non empty a_partition of X

for A being Subset of D holds (proj D) " A = union A

let D be non empty a_partition of X; :: thesis: for A being Subset of D holds (proj D) " A = union A

let A be Subset of D; :: thesis: (proj D) " A = union A

thus (proj D) " A c= union A :: according to XBOOLE_0:def 10 :: thesis: union A c= (proj D) " A

assume e in union A ; :: thesis: e in (proj D) " A

then consider u being set such that

A1: e in u and

A2: u in A by TARSKI:def 4;

A3: u in D by A2;

then (proj D) . e = u by A1, Th65;

hence e in (proj D) " A by A1, A2, A3, FUNCT_2:38; :: thesis: verum

for A being Subset of D holds (proj D) " A = union A

let D be non empty a_partition of X; :: thesis: for A being Subset of D holds (proj D) " A = union A

let A be Subset of D; :: thesis: (proj D) " A = union A

thus (proj D) " A c= union A :: according to XBOOLE_0:def 10 :: thesis: union A c= (proj D) " A

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in union A or e in (proj D) " A )
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in (proj D) " A or e in union A )

assume e in (proj D) " A ; :: thesis: e in union A

then ( (proj D) . e in A & e in (proj D) . e ) by Def9, FUNCT_2:38;

hence e in union A by TARSKI:def 4; :: thesis: verum

end;assume e in (proj D) " A ; :: thesis: e in union A

then ( (proj D) . e in A & e in (proj D) . e ) by Def9, FUNCT_2:38;

hence e in union A by TARSKI:def 4; :: thesis: verum

assume e in union A ; :: thesis: e in (proj D) " A

then consider u being set such that

A1: e in u and

A2: u in A by TARSKI:def 4;

A3: u in D by A2;

then (proj D) . e = u by A1, Th65;

hence e in (proj D) " A by A1, A2, A3, FUNCT_2:38; :: thesis: verum