let a be Real; :: thesis: for A being closed-interval Subset of REAL
for g, f1, f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( g . x = 1 & f1 . x = x / a & f1 . x > - 1 & f1 . x < 1 ) ) & Z = dom f & f | A is continuous & f = (arcsin * f1) + ((id Z) / (a (#) ((#R (1 / 2)) * (g - (f1 ^2 ))))) holds
integral f,A = (((id Z) (#) (arcsin * f1)) . (sup A)) - (((id Z) (#) (arcsin * f1)) . (inf A))
let A be closed-interval Subset of REAL ; :: thesis: for g, f1, f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( g . x = 1 & f1 . x = x / a & f1 . x > - 1 & f1 . x < 1 ) ) & Z = dom f & f | A is continuous & f = (arcsin * f1) + ((id Z) / (a (#) ((#R (1 / 2)) * (g - (f1 ^2 ))))) holds
integral f,A = (((id Z) (#) (arcsin * f1)) . (sup A)) - (((id Z) (#) (arcsin * f1)) . (inf A))
let g, f1, f be PartFunc of REAL ,REAL ; :: thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( g . x = 1 & f1 . x = x / a & f1 . x > - 1 & f1 . x < 1 ) ) & Z = dom f & f | A is continuous & f = (arcsin * f1) + ((id Z) / (a (#) ((#R (1 / 2)) * (g - (f1 ^2 ))))) holds
integral f,A = (((id Z) (#) (arcsin * f1)) . (sup A)) - (((id Z) (#) (arcsin * f1)) . (inf A))
let Z be open Subset of REAL ; :: thesis: ( A c= Z & ( for x being Real st x in Z holds
( g . x = 1 & f1 . x = x / a & f1 . x > - 1 & f1 . x < 1 ) ) & Z = dom f & f | A is continuous & f = (arcsin * f1) + ((id Z) / (a (#) ((#R (1 / 2)) * (g - (f1 ^2 ))))) implies integral f,A = (((id Z) (#) (arcsin * f1)) . (sup A)) - (((id Z) (#) (arcsin * f1)) . (inf A)) )
assume A1: ( A c= Z & ( for x being Real st x in Z holds
( g . x = 1 & f1 . x = x / a & f1 . x > - 1 & f1 . x < 1 ) ) & Z = dom f & f | A is continuous & f = (arcsin * f1) + ((id Z) / (a (#) ((#R (1 / 2)) * (g - (f1 ^2 ))))) ) ; :: thesis: integral f,A = (((id Z) (#) (arcsin * f1)) . (sup A)) - (((id Z) (#) (arcsin * f1)) . (inf A))
A2: Z = (dom (arcsin * f1)) /\ (dom ((id Z) / (a (#) ((#R (1 / 2)) * (g - (f1 ^2 )))))) by VALUED_1:def 1, A1;
A3: ( Z c= dom (arcsin * f1) & Z c= dom ((id Z) / (a (#) ((#R (1 / 2)) * (g - (f1 ^2 ))))) ) by XBOOLE_1:18, A2;
Z = dom (id Z) by RELAT_1:71;
then A4: Z c= (dom (id Z)) /\ (dom (arcsin * f1)) by A3, XBOOLE_1:19;
A5: Z c= dom ((id Z) (#) (arcsin * f1)) by VALUED_1:def 4, A4;
Z c= (dom (id Z)) /\ ((dom (a (#) ((#R (1 / 2)) * (g - (f1 ^2 ))))) \ ((a (#) ((#R (1 / 2)) * (g - (f1 ^2 )))) " {0 })) by A3, RFUNCT_1:def 4;
then A6: Z c= (dom (a (#) ((#R (1 / 2)) * (g - (f1 ^2 ))))) \ ((a (#) ((#R (1 / 2)) * (g - (f1 ^2 )))) " {0 }) by XBOOLE_1:18;
A7: Z c= dom ((a (#) ((#R (1 / 2)) * (g - (f1 ^2 )))) ^ ) by RFUNCT_1:def 8, A6;
dom ((a (#) ((#R (1 / 2)) * (g - (f1 ^2 )))) ^ ) c= dom (a (#) ((#R (1 / 2)) * (g - (f1 ^2 )))) by RFUNCT_1:11;
then A8: Z c= dom (a (#) ((#R (1 / 2)) * (g - (f1 ^2 )))) by XBOOLE_1:1, A7;
A9: Z c= dom ((#R (1 / 2)) * (g - (f1 ^2 ))) by VALUED_1:def 5, A8;
A10: ( f is_integrable_on A & f | A is bounded ) by A1, INTEGRA5:10, INTEGRA5:11;
A11: for x being Real st x in Z holds
( f1 . x = x / a & f1 . x > - 1 & f1 . x < 1 ) by A1;
then A12: (id Z) (#) (arcsin * f1) is_differentiable_on Z by A5, FDIFF_7:25;
A13: for x being Real st x in Z holds
f . x = (arcsin . (x / a)) + (x / (a * (sqrt (1 - ((x / a) ^2 )))))

proof

let x be Real; :: thesis: ( x in Z implies f . x = (arcsin . (x / a)) + (x / (a * (sqrt (1 - ((x / a) ^2 ))))) )
assume A14: x in Z ; :: thesis: f . x = (arcsin . (x / a)) + (x / (a * (sqrt (1 - ((x / a) ^2 )))))
A15: ( x in dom (g - (f1 ^2 )) & (g - (f1 ^2 )) . x in dom (#R (1 / 2)) ) by FUNCT_1:21, A14, A9;
A16: (g - (f1 ^2 )) . x in right_open_halfline 0 by A15, TAYLOR_1:def 4;
( - 1 < f1 . x & f1 . x < 1 ) by A1, A14;
then ( 0 < 1 + (f1 . x) & 0 < 1 - (f1 . x) ) by XREAL_1:150, XREAL_1:52;
then A18: 0 < (1 + (f1 . x)) * (1 - (f1 . x)) by XREAL_1:131;
aa: f1 . x = x / a by A1, A14;
((arcsin * f1) + ((id Z) / (a (#) ((#R (1 / 2)) * (g - (f1 ^2 )))))) . x = ((arcsin * f1) . x) + (((id Z) / (a (#) ((#R (1 / 2)) * (g - (f1 ^2 ))))) . x) by VALUED_1:def 1, A1, A14
.= (arcsin . (f1 . x)) + (((id Z) / (a (#) ((#R (1 / 2)) * (g - (f1 ^2 ))))) . x) by FUNCT_1:22, A3, A14
.= (arcsin . (x / a)) + (((id Z) / (a (#) ((#R (1 / 2)) * (g - (f1 ^2 ))))) . x) by A1, A14
.= (arcsin . (x / a)) + (((id Z) . x) / ((a (#) ((#R (1 / 2)) * (g - (f1 ^2 )))) . x)) by RFUNCT_1:def 4, A3, A14
.= (arcsin . (x / a)) + (x / ((a (#) ((#R (1 / 2)) * (g - (f1 ^2 )))) . x)) by FUNCT_1:35, A14
.= (arcsin . (x / a)) + (x / (a * (((#R (1 / 2)) * (g - (f1 ^2 ))) . x))) by VALUED_1:6
.= (arcsin . (x / a)) + (x / (a * ((#R (1 / 2)) . ((g - (f1 ^2 )) . x)))) by A9, FUNCT_1:22, A14
.= (arcsin . (x / a)) + (x / (a * (((g - (f1 ^2 )) . x) #R (1 / 2)))) by TAYLOR_1:def 4, A16
.= (arcsin . (x / a)) + (x / (a * (((g . x) - ((f1 ^2 ) . x)) #R (1 / 2)))) by VALUED_1:13, A15
.= (arcsin . (x / a)) + (x / (a * (((g . x) - ((f1 . x) ^2 )) #R (1 / 2)))) by VALUED_1:11
.= (arcsin . (x / a)) + (x / (a * ((1 - ((f1 . x) ^2 )) #R (1 / 2)))) by A1, A14
.= (arcsin . (x / a)) + (x / (a * ((1 - ((x / a) ^2 )) #R (1 / 2)))) by A1, A14
.= (arcsin . (x / a)) + (x / (a * (sqrt (1 - ((x / a) ^2 ))))) by FDIFF_7:2, aa, A18 ;
hence f . x = (arcsin . (x / a)) + (x / (a * (sqrt (1 - ((x / a) ^2 ))))) by A1; :: thesis: verum

end;

A20: for x being Real st x in dom (((id Z) (#) (arcsin * f1)) `| Z) holds
(((id Z) (#) (arcsin * f1)) `| Z) . x = f . x

proof

let x be Real; :: thesis: ( x in dom (((id Z) (#) (arcsin * f1)) `| Z) implies (((id Z) (#) (arcsin * f1)) `| Z) . x = f . x )
assume x in dom (((id Z) (#) (arcsin * f1)) `| Z) ; :: thesis: (((id Z) (#) (arcsin * f1)) `| Z) . x = f . x
then A21: x in Z by A12, FDIFF_1:def 8;
then (((id Z) (#) (arcsin * f1)) `| Z) . x = (arcsin . (x / a)) + (x / (a * (sqrt (1 - ((x / a) ^2 ))))) by A5, A11, FDIFF_7:25
.= f . x by A13, A21 ;
hence (((id Z) (#) (arcsin * f1)) `| Z) . x = f . x ; :: thesis: verum

end;

dom (((id Z) (#) (arcsin * f1)) `| Z) = dom f by A1, A12, FDIFF_1:def 8;
then ((id Z) (#) (arcsin * f1)) `| Z = f by A20, PARTFUN1:34;
hence integral f,A = (((id Z) (#) (arcsin * f1)) . (sup A)) - (((id Z) (#) (arcsin * f1)) . (inf A)) by A1, A10, A12, INTEGRA5:13; :: thesis: verum