let X be Complex_Banach_Algebra; :: thesis: for x being Point of X st ||.((1. X) - x).|| < 1 holds
( x is invertible & x " = Sum (((1. X) - x) GeoSeq ) )
let x be Point of X; :: thesis: ( ||.((1. X) - x).|| < 1 implies ( x is invertible & x " = Sum (((1. X) - x) GeoSeq ) ) )
assume A1: ||.((1. X) - x).|| < 1 ; :: thesis: ( x is invertible & x " = Sum (((1. X) - x) GeoSeq ) )
set seq = ((1. X) - x) GeoSeq ;
A2: ((1. X) - x) GeoSeq is summable by A1, Th44;
then A3: ||.((((1. X) - x) GeoSeq ) ^\ 1).|| is convergent by CLOPBAN1:45;
reconsider y = Sum (((1. X) - x) GeoSeq ) as Element of X ;
A4: Partial_Sums (((1. X) - x) GeoSeq ) is convergent by A2, Def2;
then lim ||.((Partial_Sums (((1. X) - x) GeoSeq )) - y).|| = 0 by CLVECT_1:120;
then A5: lim (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq )) - y).||) = ||.x.|| * 0 by A4, CLVECT_1:120, SEQ_2:22
.= 0 ;
lim ((((1. X) - x) GeoSeq ) ^\ 1) = 0. X by A2, Th18;
then A6: lim ||.((((1. X) - x) GeoSeq ) ^\ 1).|| = ||.(0. X).|| by A2, CLOPBAN1:45;
A7: ||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq )) - y).|| is convergent by A4, CLVECT_1:120, SEQ_2:21;
then A8: ||.((((1. X) - x) GeoSeq ) ^\ 1).|| + (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq )) - y).||) is convergent by A3, SEQ_2:19;
A9: lim (||.((((1. X) - x) GeoSeq ) ^\ 1).|| + (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq )) - y).||)) = (lim ||.((((1. X) - x) GeoSeq ) ^\ 1).||) + (lim (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq )) - y).||)) by A7, A3, SEQ_2:20
.= 0 by A5, A6, CLVECT_1:103 ;
A10: for n being Element of NAT holds ((1. X) - x) * ((((1. X) - x) GeoSeq ) . n) = (((1. X) - x) GeoSeq ) . (n + 1)

proof

defpred S₁[ Element of NAT ] means ((1. X) - x) * ((((1. X) - x) GeoSeq ) . $1) = (((1. X) - x) GeoSeq ) . ($1 + 1);
A11: ((1. X) - x) * ((((1. X) - x) GeoSeq ) . 0 ) = ((1. X) - x) * (1. X) by Def12
.= (1. X) - x by Th42 ;
A12: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A13: S₁[k] ; :: thesis: S₁[k + 1]
thus ((1. X) - x) * ((((1. X) - x) GeoSeq ) . (k + 1)) = ((1. X) - x) * (((((1. X) - x) GeoSeq ) . k) * ((1. X) - x)) by Def12
.= (((1. X) - x) * ((((1. X) - x) GeoSeq ) . k)) * ((1. X) - x) by Th42
.= (((1. X) - x) GeoSeq ) . ((k + 1) + 1) by A13, Def12 ; :: thesis: verum

end;

(((1. X) - x) GeoSeq ) . (0 + 1) = ((((1. X) - x) GeoSeq ) . 0 ) * ((1. X) - x) by Def12
.= (1. X) * ((1. X) - x) by Def12
.= (1. X) - x by Th42 ;
then A14: S₁[ 0 ] by A11;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A14, A12);
hence for n being Element of NAT holds ((1. X) - x) * ((((1. X) - x) GeoSeq ) . n) = (((1. X) - x) GeoSeq ) . (n + 1) ; :: thesis: verum

end;

A15: for n being Element of NAT holds ((1. X) - x) * ((Partial_Sums (((1. X) - x) GeoSeq )) . n) = (((Partial_Sums (((1. X) - x) GeoSeq )) ^\ 1) . n) - ((((1. X) - x) GeoSeq ) . 0 )

proof

defpred S₁[ Element of NAT ] means ((1. X) - x) * ((Partial_Sums (((1. X) - x) GeoSeq )) . $1) = (((Partial_Sums (((1. X) - x) GeoSeq )) ^\ 1) . $1) - ((((1. X) - x) GeoSeq ) . 0 );
A16: ((1. X) - x) * ((Partial_Sums (((1. X) - x) GeoSeq )) . 0 ) = ((1. X) - x) * ((((1. X) - x) GeoSeq ) . 0 ) by BHSP_4:def 1
.= ((1. X) - x) * (1. X) by Def12
.= (1. X) - x by Th42 ;
A17: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A18: S₁[k] ; :: thesis: S₁[k + 1]
A19: (((Partial_Sums (((1. X) - x) GeoSeq )) ^\ 1) . (k + 1)) - ((((1. X) - x) GeoSeq ) . 0 ) = ((Partial_Sums (((1. X) - x) GeoSeq )) . ((k + 1) + 1)) - ((((1. X) - x) GeoSeq ) . 0 ) by NAT_1:def 3
.= (((Partial_Sums (((1. X) - x) GeoSeq )) . (k + 1)) + ((((1. X) - x) GeoSeq ) . ((k + 1) + 1))) - ((((1. X) - x) GeoSeq ) . 0 ) by BHSP_4:def 1
.= ((((Partial_Sums (((1. X) - x) GeoSeq )) ^\ 1) . k) + ((((1. X) - x) GeoSeq ) . ((k + 1) + 1))) + (- ((((1. X) - x) GeoSeq ) . 0 )) by NAT_1:def 3
.= ((((Partial_Sums (((1. X) - x) GeoSeq )) ^\ 1) . k) - ((((1. X) - x) GeoSeq ) . 0 )) + ((((1. X) - x) GeoSeq ) . ((k + 1) + 1)) by RLVECT_1:def 6 ;
((1. X) - x) * ((Partial_Sums (((1. X) - x) GeoSeq )) . (k + 1)) = ((1. X) - x) * (((Partial_Sums (((1. X) - x) GeoSeq )) . k) + ((((1. X) - x) GeoSeq ) . (k + 1))) by BHSP_4:def 1
.= (((1. X) - x) * ((Partial_Sums (((1. X) - x) GeoSeq )) . k)) + (((1. X) - x) * ((((1. X) - x) GeoSeq ) . (k + 1))) by Th42
.= ((((Partial_Sums (((1. X) - x) GeoSeq )) ^\ 1) . k) - ((((1. X) - x) GeoSeq ) . 0 )) + ((((1. X) - x) GeoSeq ) . ((k + 1) + 1)) by A10, A18 ;
hence S₁[k + 1] by A19; :: thesis: verum

end;

(((Partial_Sums (((1. X) - x) GeoSeq )) ^\ 1) . 0 ) - ((((1. X) - x) GeoSeq ) . 0 ) = ((Partial_Sums (((1. X) - x) GeoSeq )) . (0 + 1)) - ((((1. X) - x) GeoSeq ) . 0 ) by NAT_1:def 3
.= (((Partial_Sums (((1. X) - x) GeoSeq )) . 0 ) + ((((1. X) - x) GeoSeq ) . 1)) - ((((1. X) - x) GeoSeq ) . 0 ) by BHSP_4:def 1
.= (((((1. X) - x) GeoSeq ) . 0 ) + ((((1. X) - x) GeoSeq ) . 1)) - ((((1. X) - x) GeoSeq ) . 0 ) by BHSP_4:def 1
.= ((((1. X) - x) GeoSeq ) . 1) + (((((1. X) - x) GeoSeq ) . 0 ) - ((((1. X) - x) GeoSeq ) . 0 )) by Th42
.= ((((1. X) - x) GeoSeq ) . 1) + (0. X) by RLVECT_1:28
.= (((1. X) - x) GeoSeq ) . (0 + 1) by RLVECT_1:10
.= ((((1. X) - x) GeoSeq ) . 0 ) * ((1. X) - x) by Def12
.= (1. X) * ((1. X) - x) by Def12
.= (1. X) - x by Th42 ;
then A20: S₁[ 0 ] by A16;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A20, A17);
hence for n being Element of NAT holds ((1. X) - x) * ((Partial_Sums (((1. X) - x) GeoSeq )) . n) = (((Partial_Sums (((1. X) - x) GeoSeq )) ^\ 1) . n) - ((((1. X) - x) GeoSeq ) . 0 ) ; :: thesis: verum

end;

now

let n be Element of NAT ; :: thesis: ||.((1. X) - (x * y)).|| <= (||.((((1. X) - x) GeoSeq ) ^\ 1).|| + (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq )) - y).||)) . n
reconsider yn = (Partial_Sums (((1. X) - x) GeoSeq )) . n as Element of X ;
(Partial_Sums (((1. X) - x) GeoSeq )) . (n + 1) = ((Partial_Sums (((1. X) - x) GeoSeq )) . n) + ((((1. X) - x) GeoSeq ) . (n + 1)) by BHSP_4:def 1;
then A21: (Partial_Sums (((1. X) - x) GeoSeq )) . (n + 1) = ((Partial_Sums (((1. X) - x) GeoSeq )) . n) + (((((1. X) - x) GeoSeq ) ^\ 1) . n) by NAT_1:def 3;
((1. X) - ((1. X) - x)) * yn = ((1. X) * yn) - (((1. X) - x) * yn) by Th42
.= yn - (((1. X) - x) * yn) by Th42
.= ((Partial_Sums (((1. X) - x) GeoSeq )) . n) - ((((Partial_Sums (((1. X) - x) GeoSeq )) ^\ 1) . n) - ((((1. X) - x) GeoSeq ) . 0 )) by A15
.= (((Partial_Sums (((1. X) - x) GeoSeq )) . n) - (((Partial_Sums (((1. X) - x) GeoSeq )) ^\ 1) . n)) + ((((1. X) - x) GeoSeq ) . 0 ) by Th42 ;
then ((1. X) - ((1. X) - x)) * yn = (((Partial_Sums (((1. X) - x) GeoSeq )) . n) - (((Partial_Sums (((1. X) - x) GeoSeq )) . n) + (((((1. X) - x) GeoSeq ) ^\ 1) . n))) + ((((1. X) - x) GeoSeq ) . 0 ) by A21, NAT_1:def 3
.= ((((Partial_Sums (((1. X) - x) GeoSeq )) . n) - ((Partial_Sums (((1. X) - x) GeoSeq )) . n)) - (((((1. X) - x) GeoSeq ) ^\ 1) . n)) + ((((1. X) - x) GeoSeq ) . 0 ) by Th42
.= ((0. X) - (((((1. X) - x) GeoSeq ) ^\ 1) . n)) + ((((1. X) - x) GeoSeq ) . 0 ) by RLVECT_1:28
.= (0. X) - ((((((1. X) - x) GeoSeq ) ^\ 1) . n) - ((((1. X) - x) GeoSeq ) . 0 )) by RLVECT_1:43
.= - ((((((1. X) - x) GeoSeq ) ^\ 1) . n) - ((((1. X) - x) GeoSeq ) . 0 )) by RLVECT_1:27
.= ((((1. X) - x) GeoSeq ) . 0 ) - (((((1. X) - x) GeoSeq ) ^\ 1) . n) by RLVECT_1:47
.= ((((1. X) - x) GeoSeq ) . 0 ) - ((((1. X) - x) GeoSeq ) . (n + 1)) by NAT_1:def 3
.= (1. X) - ((((1. X) - x) GeoSeq ) . (n + 1)) by Def12 ;
then A22: (1. X) - (x * yn) = (1. X) - ((1. X) - ((((1. X) - x) GeoSeq ) . (n + 1))) by Th42
.= (((1. X) - x) GeoSeq ) . (n + 1) by Th42
.= ((((1. X) - x) GeoSeq ) ^\ 1) . n by NAT_1:def 3 ;
||.(x * (yn - y)).|| <= ||.x.|| * ||.(yn - y).|| by Th42;
then A23: (||.((((1. X) - x) GeoSeq ) ^\ 1).|| . n) + ||.(x * (yn - y)).|| <= (||.((((1. X) - x) GeoSeq ) ^\ 1).|| . n) + (||.x.|| * ||.(yn - y).||) by XREAL_1:9;
( ||.((((((1. X) - x) GeoSeq ) ^\ 1) . n) + (x * (yn - y))).|| <= ||.(((((1. X) - x) GeoSeq ) ^\ 1) . n).|| + ||.(x * (yn - y)).|| & ||.(((((1. X) - x) GeoSeq ) ^\ 1) . n).|| + ||.(x * (yn - y)).|| = (||.((((1. X) - x) GeoSeq ) ^\ 1).|| . n) + ||.(x * (yn - y)).|| ) by CLVECT_1:def 11, CLVECT_1:def 17;
then A24: ||.((((((1. X) - x) GeoSeq ) ^\ 1) . n) + (x * (yn - y))).|| <= (||.((((1. X) - x) GeoSeq ) ^\ 1).|| . n) + (||.x.|| * ||.(yn - y).||) by A23, XXREAL_0:2;
(1. X) - (x * y) = ((1. X) - (0. X)) - (x * y) by RLVECT_1:26
.= ((1. X) - ((x * yn) - (x * yn))) - (x * y) by RLVECT_1:28
.= (((1. X) - (x * yn)) + (x * yn)) - (x * y) by RLVECT_1:43
.= ((1. X) - (x * yn)) + ((x * yn) - (x * y)) by RLVECT_1:def 6
.= ((1. X) - (x * yn)) + (x * (yn - y)) by Th42 ;
then ||.((1. X) - (x * y)).|| <= (||.((((1. X) - x) GeoSeq ) ^\ 1).|| . n) + (||.x.|| * ||.(((Partial_Sums (((1. X) - x) GeoSeq )) - y) . n).||) by A22, A24, NORMSP_1:def 7;
then ||.((1. X) - (x * y)).|| <= (||.((((1. X) - x) GeoSeq ) ^\ 1).|| . n) + (||.x.|| * (||.((Partial_Sums (((1. X) - x) GeoSeq )) - y).|| . n)) by CLVECT_1:def 17;
then ||.((1. X) - (x * y)).|| <= (||.((((1. X) - x) GeoSeq ) ^\ 1).|| . n) + ((||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq )) - y).||) . n) by SEQ_1:13;
hence ||.((1. X) - (x * y)).|| <= (||.((((1. X) - x) GeoSeq ) ^\ 1).|| + (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq )) - y).||)) . n by SEQ_1:11; :: thesis: verum

end;

then A25: 1. X = x * y by A8, A9, Lm3;
A26: for n being Element of NAT holds ((Partial_Sums (((1. X) - x) GeoSeq )) . n) * ((1. X) - x) = (((Partial_Sums (((1. X) - x) GeoSeq )) ^\ 1) . n) - ((((1. X) - x) GeoSeq ) . 0 )

proof

defpred S₁[ Element of NAT ] means ((Partial_Sums (((1. X) - x) GeoSeq )) . $1) * ((1. X) - x) = (((Partial_Sums (((1. X) - x) GeoSeq )) ^\ 1) . $1) - ((((1. X) - x) GeoSeq ) . 0 );
A27: ((Partial_Sums (((1. X) - x) GeoSeq )) . 0 ) * ((1. X) - x) = ((((1. X) - x) GeoSeq ) . 0 ) * ((1. X) - x) by BHSP_4:def 1
.= (1. X) * ((1. X) - x) by Def12
.= (1. X) - x by Th42 ;
A28: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A29: S₁[k] ; :: thesis: S₁[k + 1]
A30: (((Partial_Sums (((1. X) - x) GeoSeq )) ^\ 1) . (k + 1)) - ((((1. X) - x) GeoSeq ) . 0 ) = ((Partial_Sums (((1. X) - x) GeoSeq )) . ((k + 1) + 1)) - ((((1. X) - x) GeoSeq ) . 0 ) by NAT_1:def 3
.= (((Partial_Sums (((1. X) - x) GeoSeq )) . (k + 1)) + ((((1. X) - x) GeoSeq ) . ((k + 1) + 1))) - ((((1. X) - x) GeoSeq ) . 0 ) by BHSP_4:def 1
.= ((((Partial_Sums (((1. X) - x) GeoSeq )) ^\ 1) . k) + ((((1. X) - x) GeoSeq ) . ((k + 1) + 1))) + (- ((((1. X) - x) GeoSeq ) . 0 )) by NAT_1:def 3
.= ((((Partial_Sums (((1. X) - x) GeoSeq )) ^\ 1) . k) - ((((1. X) - x) GeoSeq ) . 0 )) + ((((1. X) - x) GeoSeq ) . ((k + 1) + 1)) by RLVECT_1:def 6 ;
((Partial_Sums (((1. X) - x) GeoSeq )) . (k + 1)) * ((1. X) - x) = (((Partial_Sums (((1. X) - x) GeoSeq )) . k) + ((((1. X) - x) GeoSeq ) . (k + 1))) * ((1. X) - x) by BHSP_4:def 1
.= (((Partial_Sums (((1. X) - x) GeoSeq )) . k) * ((1. X) - x)) + (((((1. X) - x) GeoSeq ) . (k + 1)) * ((1. X) - x)) by Th42
.= ((((Partial_Sums (((1. X) - x) GeoSeq )) ^\ 1) . k) - ((((1. X) - x) GeoSeq ) . 0 )) + ((((1. X) - x) GeoSeq ) . ((k + 1) + 1)) by A29, Def12 ;
hence S₁[k + 1] by A30; :: thesis: verum

end;

(((Partial_Sums (((1. X) - x) GeoSeq )) ^\ 1) . 0 ) - ((((1. X) - x) GeoSeq ) . 0 ) = ((Partial_Sums (((1. X) - x) GeoSeq )) . (0 + 1)) - ((((1. X) - x) GeoSeq ) . 0 ) by NAT_1:def 3
.= (((Partial_Sums (((1. X) - x) GeoSeq )) . 0 ) + ((((1. X) - x) GeoSeq ) . 1)) - ((((1. X) - x) GeoSeq ) . 0 ) by BHSP_4:def 1
.= (((((1. X) - x) GeoSeq ) . 0 ) + ((((1. X) - x) GeoSeq ) . 1)) - ((((1. X) - x) GeoSeq ) . 0 ) by BHSP_4:def 1
.= ((((1. X) - x) GeoSeq ) . 1) + (((((1. X) - x) GeoSeq ) . 0 ) - ((((1. X) - x) GeoSeq ) . 0 )) by Th42
.= ((((1. X) - x) GeoSeq ) . 1) + (0. X) by RLVECT_1:28
.= (((1. X) - x) GeoSeq ) . (0 + 1) by RLVECT_1:10
.= ((((1. X) - x) GeoSeq ) . 0 ) * ((1. X) - x) by Def12
.= (1. X) * ((1. X) - x) by Def12
.= (1. X) - x by Th42 ;
then A31: S₁[ 0 ] by A27;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A31, A28);
hence for n being Element of NAT holds ((Partial_Sums (((1. X) - x) GeoSeq )) . n) * ((1. X) - x) = (((Partial_Sums (((1. X) - x) GeoSeq )) ^\ 1) . n) - ((((1. X) - x) GeoSeq ) . 0 ) ; :: thesis: verum

end;

now

let n be Element of NAT ; :: thesis: ||.((1. X) - (y * x)).|| <= (||.((((1. X) - x) GeoSeq ) ^\ 1).|| + (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq )) - y).||)) . n
reconsider yn = (Partial_Sums (((1. X) - x) GeoSeq )) . n as Element of X ;
(Partial_Sums (((1. X) - x) GeoSeq )) . (n + 1) = ((Partial_Sums (((1. X) - x) GeoSeq )) . n) + ((((1. X) - x) GeoSeq ) . (n + 1)) by BHSP_4:def 1;
then A32: (Partial_Sums (((1. X) - x) GeoSeq )) . (n + 1) = ((Partial_Sums (((1. X) - x) GeoSeq )) . n) + (((((1. X) - x) GeoSeq ) ^\ 1) . n) by NAT_1:def 3;
yn * ((1. X) - ((1. X) - x)) = (yn * (1. X)) - (yn * ((1. X) - x)) by Th42
.= yn - (yn * ((1. X) - x)) by Th42
.= ((Partial_Sums (((1. X) - x) GeoSeq )) . n) - ((((Partial_Sums (((1. X) - x) GeoSeq )) ^\ 1) . n) - ((((1. X) - x) GeoSeq ) . 0 )) by A26
.= (((Partial_Sums (((1. X) - x) GeoSeq )) . n) - (((Partial_Sums (((1. X) - x) GeoSeq )) ^\ 1) . n)) + ((((1. X) - x) GeoSeq ) . 0 ) by Th42 ;
then yn * ((1. X) - ((1. X) - x)) = (((Partial_Sums (((1. X) - x) GeoSeq )) . n) - (((Partial_Sums (((1. X) - x) GeoSeq )) . n) + (((((1. X) - x) GeoSeq ) ^\ 1) . n))) + ((((1. X) - x) GeoSeq ) . 0 ) by A32, NAT_1:def 3
.= ((((Partial_Sums (((1. X) - x) GeoSeq )) . n) - ((Partial_Sums (((1. X) - x) GeoSeq )) . n)) - (((((1. X) - x) GeoSeq ) ^\ 1) . n)) + ((((1. X) - x) GeoSeq ) . 0 ) by Th42
.= ((0. X) - (((((1. X) - x) GeoSeq ) ^\ 1) . n)) + ((((1. X) - x) GeoSeq ) . 0 ) by RLVECT_1:28
.= (0. X) - ((((((1. X) - x) GeoSeq ) ^\ 1) . n) - ((((1. X) - x) GeoSeq ) . 0 )) by RLVECT_1:43
.= - ((((((1. X) - x) GeoSeq ) ^\ 1) . n) - ((((1. X) - x) GeoSeq ) . 0 )) by RLVECT_1:27
.= ((((1. X) - x) GeoSeq ) . 0 ) - (((((1. X) - x) GeoSeq ) ^\ 1) . n) by RLVECT_1:47
.= ((((1. X) - x) GeoSeq ) . 0 ) - ((((1. X) - x) GeoSeq ) . (n + 1)) by NAT_1:def 3
.= (1. X) - ((((1. X) - x) GeoSeq ) . (n + 1)) by Def12 ;
then A33: (1. X) - (yn * x) = (1. X) - ((1. X) - ((((1. X) - x) GeoSeq ) . (n + 1))) by Th42
.= (((1. X) - x) GeoSeq ) . (n + 1) by Th42
.= ((((1. X) - x) GeoSeq ) ^\ 1) . n by NAT_1:def 3 ;
||.((yn - y) * x).|| <= ||.(yn - y).|| * ||.x.|| by Th42;
then A34: (||.((((1. X) - x) GeoSeq ) ^\ 1).|| . n) + ||.((yn - y) * x).|| <= (||.((((1. X) - x) GeoSeq ) ^\ 1).|| . n) + (||.(yn - y).|| * ||.x.||) by XREAL_1:9;
( ||.((((((1. X) - x) GeoSeq ) ^\ 1) . n) + ((yn - y) * x)).|| <= ||.(((((1. X) - x) GeoSeq ) ^\ 1) . n).|| + ||.((yn - y) * x).|| & ||.(((((1. X) - x) GeoSeq ) ^\ 1) . n).|| + ||.((yn - y) * x).|| = (||.((((1. X) - x) GeoSeq ) ^\ 1).|| . n) + ||.((yn - y) * x).|| ) by CLVECT_1:def 11, CLVECT_1:def 17;
then A35: ||.((((((1. X) - x) GeoSeq ) ^\ 1) . n) + ((yn - y) * x)).|| <= (||.((((1. X) - x) GeoSeq ) ^\ 1).|| . n) + (||.(yn - y).|| * ||.x.||) by A34, XXREAL_0:2;
(1. X) - (y * x) = ((1. X) - (0. X)) - (y * x) by RLVECT_1:26
.= ((1. X) - ((yn * x) - (yn * x))) - (y * x) by RLVECT_1:28
.= (((1. X) - (yn * x)) + (yn * x)) - (y * x) by RLVECT_1:43
.= ((1. X) - (yn * x)) + ((yn * x) - (y * x)) by RLVECT_1:def 6
.= ((1. X) - (yn * x)) + ((yn - y) * x) by Th42 ;
then ||.((1. X) - (y * x)).|| <= (||.((((1. X) - x) GeoSeq ) ^\ 1).|| . n) + (||.(((Partial_Sums (((1. X) - x) GeoSeq )) - y) . n).|| * ||.x.||) by A33, A35, NORMSP_1:def 7;
then ||.((1. X) - (y * x)).|| <= (||.((((1. X) - x) GeoSeq ) ^\ 1).|| . n) + ((||.((Partial_Sums (((1. X) - x) GeoSeq )) - y).|| . n) * ||.x.||) by CLVECT_1:def 17;
then ||.((1. X) - (y * x)).|| <= (||.((((1. X) - x) GeoSeq ) ^\ 1).|| . n) + ((||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq )) - y).||) . n) by SEQ_1:13;
hence ||.((1. X) - (y * x)).|| <= (||.((((1. X) - x) GeoSeq ) ^\ 1).|| + (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq )) - y).||)) . n by SEQ_1:11; :: thesis: verum

end;

then A36: 1. X = y * x by A8, A9, Lm3;
hence x is invertible by A25, LOPBAN_3:def 8; :: thesis: x " = Sum (((1. X) - x) GeoSeq )
hence x " = Sum (((1. X) - x) GeoSeq ) by A36, A25, LOPBAN_3:def 12; :: thesis: verum