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 ;
( 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))
;
((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;
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; verum