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

end;

dom (proj1 * ((Sq_Circ " ) | K1)) c= dom ((Sq_Circ " ) | K1) by RELAT_1:44;
then dom (proj1 * ((Sq_Circ " ) | K1)) = dom ((Sq_Circ " ) | K1) by A2, 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 ;
hence proj1 * ((Sq_Circ " ) | K1) is Function of ((TOP-REAL 2) | K1),R^1 by A1, FUNCT_2:4, TOPMETR:24, XBOOLE_1:1; :: thesis: verum