set T = Tcircle ((0. (TOP-REAL 2)),r);
set f = (Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r));
set C = the carrier of (Tcircle ((0. (TOP-REAL 2)),r));
A1: dom ((Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r))) = the carrier of (Tcircle ((0. (TOP-REAL 2)),r)) by FUNCT_2:def 1;
for x being object st x in the carrier of (Tcircle ((0. (TOP-REAL 2)),r)) holds
((Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r))) . x in the carrier of (Tcircle ((0. (TOP-REAL 2)),r))

proof

let x be object ; :: thesis: ( x in the carrier of (Tcircle ((0. (TOP-REAL 2)),r)) implies ((Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r))) . x in the carrier of (Tcircle ((0. (TOP-REAL 2)),r)) )
assume A2: x in the carrier of (Tcircle ((0. (TOP-REAL 2)),r)) ; :: thesis: ((Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r))) . x in the carrier of (Tcircle ((0. (TOP-REAL 2)),r))
then A3: ((Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r))) . x = (Rotate s) . x by FUNCT_1:49;
the carrier of (Tcircle ((0. (TOP-REAL 2)),r)) = Sphere ((0. (TOP-REAL 2)),r) by TOPREALB:9;
hence ((Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r))) . x in the carrier of (Tcircle ((0. (TOP-REAL 2)),r)) by A3, A2, Th48; :: thesis: verum

end;

hence (Rotate s) | (Tcircle ((0. (TOP-REAL 2)),r)) is Function of (Tcircle ((0. (TOP-REAL 2)),r)),(Tcircle ((0. (TOP-REAL 2)),r)) by A1, FUNCT_2:3; :: thesis: verum