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

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

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

dom (proj2 * ((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 (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;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

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