let x, y be Real; :: thesis: ( x ^2 < 1 & y < 1 implies (x ^2) * y < 1 )
assume that
A1: x ^2 < 1 and
A2: y < 1 ; :: thesis: (x ^2) * y < 1

per cases ( 0 = x ^2 or 0 < x ^2 ) by XREAL_1:63;

suppose 0 = x ^2 ; :: thesis: (x ^2) * y < 1

hence (x ^2) * y < 1 ; :: thesis: verum

end;

suppose 0 < x ^2 ; :: thesis: (x ^2) * y < 1

then y * (x ^2) < 1 * (x ^2) by A2, XREAL_1:68;
hence (x ^2) * y < 1 by A1, XXREAL_0:2; :: thesis: verum

end;

end;