let K1 be non empty Subset of (TOP-REAL 2); :: thesis: proj1 * ((Sq_Circ " ) | K1) is Function of ((TOP-REAL 2) | K1),R^1
A1: dom (proj1 * ((Sq_Circ " ) | K1)) c= dom ((Sq_Circ " ) | K1) by RELAT_1:44;
dom ((Sq_Circ " ) | K1) c= dom (proj1 * ((Sq_Circ " ) | K1))

proof

let x be set ; :: 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 A3: x in (dom (Sq_Circ " )) /\ K1 by RELAT_1:90;
A4: ((Sq_Circ " ) | K1) . x = (Sq_Circ " ) . x by A2, FUNCT_1:70;
x in dom (Sq_Circ " ) by A3, XBOOLE_0:def 4;
then A5: (Sq_Circ " ) . x in rng (Sq_Circ " ) by FUNCT_1:12;
rng (Sq_Circ " ) c= the carrier of (TOP-REAL 2) by Th39, RELAT_1:def 19;
hence x in dom (proj1 * ((Sq_Circ " ) | K1)) by A2, A4, A5, Lm2, FUNCT_1:21; :: thesis: verum

end;

then A6: dom (proj1 * ((Sq_Circ " ) | K1)) = dom ((Sq_Circ " ) | K1) by A1, XBOOLE_0:def 10
.= (dom (Sq_Circ " )) /\ K1 by RELAT_1:90
.= the carrier of (TOP-REAL 2) /\ K1 by Th39, FUNCT_2:def 1
.= K1 by XBOOLE_1:28
.= the carrier of ((TOP-REAL 2) | K1) by PRE_TOPC:29 ;
rng (proj1 * ((Sq_Circ " ) | K1)) c= rng proj1 by RELAT_1:45;
hence proj1 * ((Sq_Circ " ) | K1) is Function of ((TOP-REAL 2) | K1),R^1 by A6, FUNCT_2:4, TOPMETR:24, XBOOLE_1:1; :: thesis: verum