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, Th40;
then A3: ||.((((1. X) - x) GeoSeq) ^\ 1).|| is convergent by CLOPBAN1:40;
reconsider y = Sum (((1. X) - x) GeoSeq) as Element of X ;
A4: Partial_Sums (((1. X) - x) GeoSeq) is convergent by A2;
then lim ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).|| = 0 by CLVECT_1:118;
then A5: lim (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).||) = ||.x.|| * 0 by A4, CLVECT_1:118, SEQ_2:8
.= 0 ;
lim ((((1. X) - x) GeoSeq) ^\ 1) = 0. X by A2, Th14;
then A6: lim ||.((((1. X) - x) GeoSeq) ^\ 1).|| = ||.(0. X).|| by A2, CLOPBAN1:40;
A7: ||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).|| is convergent by A4, CLVECT_1:118, SEQ_2:7;
then A8: ||.((((1. X) - x) GeoSeq) ^\ 1).|| + (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).||) is convergent by A3, SEQ_2:5;
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:6
.= 0 by A5, A6 ;
A10: for n being Nat holds ((1. X) - x) * ((((1. X) - x) GeoSeq) . n) = (((1. X) - x) GeoSeq) . (n + 1)

proof

defpred S₁[ 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 Def4
.= (1. X) - x by VECTSP_1:def 4 ;
A12: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be 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 Def4
.= (((1. X) - x) * ((((1. X) - x) GeoSeq) . k)) * ((1. X) - x) by GROUP_1:def 3
.= (((1. X) - x) GeoSeq) . ((k + 1) + 1) by A13, Def4 ; :: thesis: verum

end;

(((1. X) - x) GeoSeq) . (0 + 1) = ((((1. X) - x) GeoSeq) . 0) * ((1. X) - x) by Def4
.= (1. X) * ((1. X) - x) by Def4
.= (1. X) - x by VECTSP_1:def 8 ;
then A14: S₁[ 0 ] by A11;
for n being Nat holds S₁[n] from NAT_1:sch 2(A14, A12);
hence for n being Nat holds ((1. X) - x) * ((((1. X) - x) GeoSeq) . n) = (((1. X) - x) GeoSeq) . (n + 1) ; :: thesis: verum

end;

A15: for n being 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₁[ 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 Def4
.= (1. X) - x by VECTSP_1:def 4 ;
A17: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be 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 3 ;
((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 VECTSP_1:def 2
.= ((((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 Th38
.= ((((1. X) - x) GeoSeq) . 1) + (0. X) by RLVECT_1:15
.= (((1. X) - x) GeoSeq) . (0 + 1) by RLVECT_1:4
.= ((((1. X) - x) GeoSeq) . 0) * ((1. X) - x) by Def4
.= (1. X) * ((1. X) - x) by Def4
.= (1. X) - x by VECTSP_1:def 8 ;
then A20: S₁[ 0 ] by A16;
for n being Nat holds S₁[n] from NAT_1:sch 2(A20, A17);
hence for n being 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 :: thesis: for n being Nat holds ||.((1. X) - (x * y)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| + (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).||)) . n

let n be 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 Th38
.= yn - (((1. X) - x) * yn) by VECTSP_1:def 8
.= ((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 Th38 ;
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 Th38
.= ((0. X) - (((((1. X) - x) GeoSeq) ^\ 1) . n)) + ((((1. X) - x) GeoSeq) . 0) by RLVECT_1:15
.= (0. X) - ((((((1. X) - x) GeoSeq) ^\ 1) . n) - ((((1. X) - x) GeoSeq) . 0)) by RLVECT_1:29
.= - ((((((1. X) - x) GeoSeq) ^\ 1) . n) - ((((1. X) - x) GeoSeq) . 0)) by RLVECT_1:14
.= ((((1. X) - x) GeoSeq) . 0) - (((((1. X) - x) GeoSeq) ^\ 1) . n) by RLVECT_1:33
.= ((((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 Def4 ;
then A22: (1. X) - (x * yn) = (1. X) - ((1. X) - ((((1. X) - x) GeoSeq) . (n + 1))) by Th38
.= (((1. X) - x) GeoSeq) . (n + 1) by Th38
.= ((((1. X) - x) GeoSeq) ^\ 1) . n by NAT_1:def 3 ;
||.(x * (yn - y)).|| <= ||.x.|| * ||.(yn - y).|| by Th38;
then A23: (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + ||.(x * (yn - y)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + (||.x.|| * ||.(yn - y).||) by XREAL_1:7;
( ||.((((((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 13, NORMSP_0:def 4;
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:13
.= ((1. X) - ((x * yn) - (x * yn))) - (x * y) by RLVECT_1:15
.= (((1. X) - (x * yn)) + (x * yn)) - (x * y) by RLVECT_1:29
.= ((1. X) - (x * yn)) + ((x * yn) - (x * y)) by RLVECT_1:def 3
.= ((1. X) - (x * yn)) + (x * (yn - y)) by Th38 ;
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 4;
then ||.((1. X) - (x * y)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + (||.x.|| * (||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).|| . n)) by NORMSP_0:def 4;
then ||.((1. X) - (x * y)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + ((||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).||) . n) by SEQ_1:9;
hence ||.((1. X) - (x * y)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| + (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).||)) . n by SEQ_1:7; :: thesis: verum

end;

then A25: 1. X = x * y by A8, A9, Lm3;
A26: for n being 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₁[ 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 Def4
.= (1. X) - x by VECTSP_1:def 8 ;
A28: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be 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 3 ;
((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 VECTSP_1:def 3
.= ((((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . k) - ((((1. X) - x) GeoSeq) . 0)) + ((((1. X) - x) GeoSeq) . ((k + 1) + 1)) by A29, Def4 ;
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 Th38
.= ((((1. X) - x) GeoSeq) . 1) + (0. X) by RLVECT_1:15
.= (((1. X) - x) GeoSeq) . (0 + 1) by RLVECT_1:4
.= ((((1. X) - x) GeoSeq) . 0) * ((1. X) - x) by Def4
.= (1. X) * ((1. X) - x) by Def4
.= (1. X) - x by VECTSP_1:def 8 ;
then A31: S₁[ 0 ] by A27;
for n being Nat holds S₁[n] from NAT_1:sch 2(A31, A28);
hence for n being 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 :: thesis: for n being Nat holds ||.((1. X) - (y * x)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| + (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).||)) . n

let n be 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 Th38
.= yn - (yn * ((1. X) - x)) by VECTSP_1:def 4
.= ((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 Th38 ;
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 Th38
.= ((0. X) - (((((1. X) - x) GeoSeq) ^\ 1) . n)) + ((((1. X) - x) GeoSeq) . 0) by RLVECT_1:15
.= (0. X) - ((((((1. X) - x) GeoSeq) ^\ 1) . n) - ((((1. X) - x) GeoSeq) . 0)) by RLVECT_1:29
.= - ((((((1. X) - x) GeoSeq) ^\ 1) . n) - ((((1. X) - x) GeoSeq) . 0)) by RLVECT_1:14
.= ((((1. X) - x) GeoSeq) . 0) - (((((1. X) - x) GeoSeq) ^\ 1) . n) by RLVECT_1:33
.= ((((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 Def4 ;
then A33: (1. X) - (yn * x) = (1. X) - ((1. X) - ((((1. X) - x) GeoSeq) . (n + 1))) by Th38
.= (((1. X) - x) GeoSeq) . (n + 1) by Th38
.= ((((1. X) - x) GeoSeq) ^\ 1) . n by NAT_1:def 3 ;
||.((yn - y) * x).|| <= ||.(yn - y).|| * ||.x.|| by Th38;
then A34: (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + ||.((yn - y) * x).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + (||.(yn - y).|| * ||.x.||) by XREAL_1:7;
( ||.((((((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 13, NORMSP_0:def 4;
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:13
.= ((1. X) - ((yn * x) - (yn * x))) - (y * x) by RLVECT_1:15
.= (((1. X) - (yn * x)) + (yn * x)) - (y * x) by RLVECT_1:29
.= ((1. X) - (yn * x)) + ((yn * x) - (y * x)) by RLVECT_1:def 3
.= ((1. X) - (yn * x)) + ((yn - y) * x) by Th38 ;
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 4;
then ||.((1. X) - (y * x)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + ((||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).|| . n) * ||.x.||) by NORMSP_0:def 4;
then ||.((1. X) - (y * x)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + ((||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).||) . n) by SEQ_1:9;
hence ||.((1. X) - (y * x)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| + (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).||)) . n by SEQ_1:7; :: thesis: verum

end;

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