let K1 be non empty Subset of (TOP-REAL 2); :: thesis: proj2 * ((Sq_Circ ") | K1) is Function of ((TOP-REAL 2) | K1),R^1
A1: rng (proj2 * ((Sq_Circ ") | K1)) c= rng proj2 by RELAT_1:26;
A2: dom ((Sq_Circ ") | K1) c= dom (proj2 * ((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 (proj2 * ((Sq_Circ ") | K1)) )
A3: rng (Sq_Circ ") c= the carrier of (TOP-REAL 2) by Th29, RELAT_1:def 19;
assume A4: x in dom ((Sq_Circ ") | K1) ; :: thesis: x in dom (proj2 * ((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 A5: (Sq_Circ ") . x in rng (Sq_Circ ") by FUNCT_1:3;
((Sq_Circ ") | K1) . x = (Sq_Circ ") . x by A4, FUNCT_1:47;
hence x in dom (proj2 * ((Sq_Circ ") | K1)) by A4, A5, A3, Lm3, FUNCT_1:11; :: thesis: verum

end;

dom (proj2 * ((Sq_Circ ") | K1)) c= dom ((Sq_Circ ") | K1) by RELAT_1:25;
then dom (proj2 * ((Sq_Circ ") | K1)) = dom ((Sq_Circ ") | K1) by A2
.= (dom (Sq_Circ ")) /\ K1 by RELAT_1:61
.= the carrier of (TOP-REAL 2) /\ K1 by Th29, FUNCT_2:def 1
.= K1 by XBOOLE_1:28
.= the carrier of ((TOP-REAL 2) | K1) by PRE_TOPC:8 ;
hence proj2 * ((Sq_Circ ") | K1) is Function of ((TOP-REAL 2) | K1),R^1 by A1, FUNCT_2:2, TOPMETR:17, XBOOLE_1:1; :: thesis: verum