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))

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

A1: dom (Sq_Circ | K1) c= dom (proj1 * (Sq_Circ | K1))

proof

dom (proj1 * (Sq_Circ | K1)) c= dom (Sq_Circ | K1)
by RELAT_1:25;
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;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

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