let K1 be non empty Subset of (TOP-REAL 2); :: thesis: dom (proj1 * (Sq_Circ | K1)) = the carrier of ((TOP-REAL 2) | K1)
A1: dom (Sq_Circ | K1) c= dom (proj1 * (Sq_Circ | K1))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (Sq_Circ | K1) or x in dom (proj1 * (Sq_Circ | K1)) )
assume A2: x in dom (Sq_Circ | K1) ; :: thesis: x in dom (proj1 * (Sq_Circ | K1))
then x in (dom Sq_Circ) /\ K1 by RELAT_1:61;
then x in dom Sq_Circ by XBOOLE_0:def 4;
then A3: Sq_Circ . x in rng Sq_Circ by FUNCT_1:3;
(Sq_Circ | K1) . x = Sq_Circ . x by A2, FUNCT_1:47;
hence x in dom (proj1 * (Sq_Circ | K1)) by A2, A3, Lm2, FUNCT_1:11; :: thesis: verum

end;

dom (proj1 * (Sq_Circ | K1)) c= dom (Sq_Circ | K1) by RELAT_1:25;
hence dom (proj1 * (Sq_Circ | K1)) = dom (Sq_Circ | K1) by A1
.= (dom Sq_Circ) /\ K1 by RELAT_1:61
.= the carrier of (TOP-REAL 2) /\ K1 by FUNCT_2:def 1
.= K1 by XBOOLE_1:28
.= the carrier of ((TOP-REAL 2) | K1) by PRE_TOPC:8 ;
:: thesis: verum