let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (ac | (R^1 Q)) or y in E )

assume A1: y in rng (ac | (R^1 Q)) ; :: thesis: y in E

then consider x being object such that

A2: x in dom (ac | (R^1 Q)) and

A3: (ac | (R^1 Q)) . x = y by FUNCT_1:def 3;

reconsider x = x as Real by A2;

A4: - 1 <= x by A2, Lm36, XXREAL_1:3;

A5: x < 1 by A2, Lm36, XXREAL_1:3;

A6: rng (ac | (R^1 Q)) c= rng ac by RELAT_1:70;

then y in [.0,PI.] by A1, SIN_COS6:85;

then reconsider y = y as Real ;

A7: y <= PI by A1, A6, SIN_COS6:85, XXREAL_1:1;

y = arccos . x by A2, A3, Lm36, FUNCT_1:49

.= arccos x by SIN_COS6:def 4 ;

then A8: y <> 0 by A4, A5, SIN_COS6:96;

0 <= y by A1, A6, SIN_COS6:85, XXREAL_1:1;

hence y in E by A7, A8, XXREAL_1:2; :: thesis: verum

assume A1: y in rng (ac | (R^1 Q)) ; :: thesis: y in E

then consider x being object such that

A2: x in dom (ac | (R^1 Q)) and

A3: (ac | (R^1 Q)) . x = y by FUNCT_1:def 3;

reconsider x = x as Real by A2;

A4: - 1 <= x by A2, Lm36, XXREAL_1:3;

A5: x < 1 by A2, Lm36, XXREAL_1:3;

A6: rng (ac | (R^1 Q)) c= rng ac by RELAT_1:70;

then y in [.0,PI.] by A1, SIN_COS6:85;

then reconsider y = y as Real ;

A7: y <= PI by A1, A6, SIN_COS6:85, XXREAL_1:1;

y = arccos . x by A2, A3, Lm36, FUNCT_1:49

.= arccos x by SIN_COS6:def 4 ;

then A8: y <> 0 by A4, A5, SIN_COS6:96;

0 <= y by A1, A6, SIN_COS6:85, XXREAL_1:1;

hence y in E by A7, A8, XXREAL_1:2; :: thesis: verum