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;
reconsider y = Sum (((1. X) - x) GeoSeq ) as Element of X ;
A3: 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 );
A4: ((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 ;
(((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 A5: S₁[ 0 ] by A4;
A6: 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 A7: S₁[k] ; :: thesis: S₁[k + 1]
A8: ((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 A7, Def12 ;
(((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 ;
hence S₁[k + 1] by A8; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A5, A6);
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;

A9: 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);
A10: ((1. X) - x) * ((((1. X) - x) GeoSeq ) . 0 ) = ((1. X) - x) * (1. X) by Def12
.= (1. X) - x by Th42 ;
(((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 A11: S₁[ 0 ] by A10;
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;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A11, 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;

A14: 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 );
A15: ((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 ;
(((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 A16: S₁[ 0 ] by A15;
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: ((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 A9, A18 ;
(((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 ;
hence S₁[k + 1] by A19; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A16, 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;

A20: 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 ;
A21: (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 ;
A22: 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 A3
.= (((Partial_Sums (((1. X) - x) GeoSeq )) . n) - (((Partial_Sums (((1. X) - x) GeoSeq )) ^\ 1) . n)) + ((((1. X) - x) GeoSeq ) . 0 ) by Th42 ;
(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 (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;
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 A22, 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 A23: (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 ;
A24: ||.((((((1. X) - x) GeoSeq ) ^\ 1) . n) + ((yn - y) * x)).|| <= ||.(((((1. X) - x) GeoSeq ) ^\ 1) . n).|| + ||.((yn - y) * x).|| by CLVECT_1:def 11;
A25: ||.(((((1. X) - x) GeoSeq ) ^\ 1) . n).|| + ||.((yn - y) * x).|| = (||.((((1. X) - x) GeoSeq ) ^\ 1).|| . n) + ||.((yn - y) * x).|| by CLVECT_1:def 17;
||.((yn - y) * x).|| <= ||.(yn - y).|| * ||.x.|| by Th42;
then (||.((((1. X) - x) GeoSeq ) ^\ 1).|| . n) + ||.((yn - y) * x).|| <= (||.((((1. X) - x) GeoSeq ) ^\ 1).|| . n) + (||.(yn - y).|| * ||.x.||) by XREAL_1:9;
then ||.((((((1. X) - x) GeoSeq ) ^\ 1) . n) + ((yn - y) * x)).|| <= (||.((((1. X) - x) GeoSeq ) ^\ 1).|| . n) + (||.(yn - y).|| * ||.x.||) by A24, A25, XXREAL_0:2;
then ||.((1. X) - (y * x)).|| <= (||.((((1. X) - x) GeoSeq ) ^\ 1).|| . n) + (||.(((Partial_Sums (((1. X) - x) GeoSeq )) - y) . n).|| * ||.x.||) by A21, A23, 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;

A26: 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 ;
A27: (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 ;
A28: ((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 A14
.= (((Partial_Sums (((1. X) - x) GeoSeq )) . n) - (((Partial_Sums (((1. X) - x) GeoSeq )) ^\ 1) . n)) + ((((1. X) - x) GeoSeq ) . 0 ) by Th42 ;
(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 (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;
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 A28, 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 A29: (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 ;
A30: ||.((((((1. X) - x) GeoSeq ) ^\ 1) . n) + (x * (yn - y))).|| <= ||.(((((1. X) - x) GeoSeq ) ^\ 1) . n).|| + ||.(x * (yn - y)).|| by CLVECT_1:def 11;
A31: ||.(((((1. X) - x) GeoSeq ) ^\ 1) . n).|| + ||.(x * (yn - y)).|| = (||.((((1. X) - x) GeoSeq ) ^\ 1).|| . n) + ||.(x * (yn - y)).|| by CLVECT_1:def 17;
||.(x * (yn - y)).|| <= ||.x.|| * ||.(yn - y).|| by Th42;
then (||.((((1. X) - x) GeoSeq ) ^\ 1).|| . n) + ||.(x * (yn - y)).|| <= (||.((((1. X) - x) GeoSeq ) ^\ 1).|| . n) + (||.x.|| * ||.(yn - y).||) by XREAL_1:9;
then ||.((((((1. X) - x) GeoSeq ) ^\ 1) . n) + (x * (yn - y))).|| <= (||.((((1. X) - x) GeoSeq ) ^\ 1).|| . n) + (||.x.|| * ||.(yn - y).||) by A30, A31, XXREAL_0:2;
then ||.((1. X) - (x * y)).|| <= (||.((((1. X) - x) GeoSeq ) ^\ 1).|| . n) + (||.x.|| * ||.(((Partial_Sums (((1. X) - x) GeoSeq )) - y) . n).||) by A27, A29, 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;

Partial_Sums (((1. X) - x) GeoSeq ) is convergent by A2, Def2;
then A32: ( ||.((Partial_Sums (((1. X) - x) GeoSeq )) - y).|| is convergent & lim ||.((Partial_Sums (((1. X) - x) GeoSeq )) - y).|| = 0 ) by CLVECT_1:120;
then A33: ||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq )) - y).|| is convergent by SEQ_2:21;
A34: lim (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq )) - y).||) = ||.x.|| * 0 by A32, SEQ_2:22
.= 0 ;
( ((1. X) - x) GeoSeq is convergent & lim (((1. X) - x) GeoSeq ) = 0. X ) by A2, Th18;
then ( (((1. X) - x) GeoSeq ) ^\ 1 is convergent & lim ((((1. X) - x) GeoSeq ) ^\ 1) = 0. X ) by Th13;
then A35: ( ||.((((1. X) - x) GeoSeq ) ^\ 1).|| is convergent & lim ||.((((1. X) - x) GeoSeq ) ^\ 1).|| = ||.(0. X).|| ) by CLOPBAN1:45;
then A36: ||.((((1. X) - x) GeoSeq ) ^\ 1).|| + (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq )) - y).||) is convergent by A33, SEQ_2:19;
A37: 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 A33, A35, SEQ_2:20
.= 0 by A34, A35, CLVECT_1:103 ;
then A38: 1. X = y * x by A20, A36, Lm6;
A39: 1. X = x * y by A26, A36, A37, Lm6;
hence x is invertible by A38, LOPBAN_3:def 8; :: thesis: x " = Sum (((1. X) - x) GeoSeq )
hence x " = Sum (((1. X) - x) GeoSeq ) by A38, A39, LOPBAN_3:def 12; :: thesis: verum