let n be Nat; :: thesis:
let D be Orthogonal_Basis of n; :: thesis:
set V = RealVectSpace (Seg n);
reconsider B = D as R-orthonormal Subset of (RealVectSpace (Seg n)) by FINSEQ_2:93;

per cases ;

suppose n = 0 ; :: thesis:

hence D is Basis of RealVectSpace (Seg n) by Th19, Th51; :: thesis:

end;

suppose A2: n <> 0 ; :: thesis:

reconsider D0 = D as R-orthonormal Subset of (REAL n) ;
consider I being Basis of RealVectSpace (Seg n) such that
A3: B c= I by RLVECT_5:2;
card I = n by Th50;
then A4: I is finite ;
A5: for D2 being R-orthonormal Subset of (REAL n) st D0 c= D2 holds
D2 = D0 by Def6;

A6: now

assume that
B <> I and
A7: not I c= the carrier of (Lin B) ; :: thesis:
consider x0 being set such that
A8: x0 in I and
A9: not x0 in the carrier of (Lin B) by A7, TARSKI:def 3;
reconsider z0 = x0 as Element of REAL n by A8, FINSEQ_2:93;
not x0 in Lin B by A9, STRUCT_0:def 5;
then A10: not x0 in B by RLVECT_3:15;
consider p being FinSequence such that
A11: rng p = B and
A12: p is one-to-one by A3, A4, FINSEQ_4:58;
A13: 1 <= (len p) + 1 by NAT_1:12;
reconsider p0 = p as FinSequence of REAL n by A11, FINSEQ_1:def 4;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= (len p) + 1 implies ex q being FinSequence of REAL n st
( len q = $1 & ( $1 <= len p implies for d being Real holds not q . $1 = d * (p0 /. $1) ) & q . 1 = z0 & ( for i being Nat
for a, b being Element of REAL n st 1 <= i & i < $1 & a = q /. i & b = p0 /. i holds
( q /. (i + 1) <> 0* n & q . (i + 1) = (q /. i) - (|(a,b)| * (p0 /. i)) ) ) ) );
A14: I is linearly-independent by RLVECT_3:def 3;
A15: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A16: S₁[k] ; :: thesis:

per cases ;

suppose A17: ( 1 <= k + 1 & k + 1 <= (len p) + 1 ) ; :: thesis:

k < k + 1 by XREAL_1:29;
then A18: k < (len p) + 1 by A17, XXREAL_0:2;
A19: k <= len p by A17, XREAL_1:6;

per cases ;

suppose 1 <= k ; :: thesis:

then consider q0 being FinSequence of REAL n such that
A20: len q0 = k and
A21: 1 <= k and
k <= (len p) + 1 and
A22: ( k <= len p implies for d being Real holds not q0 . k = d * (p0 /. k) ) and
A23: q0 . 1 = z0 and
A24: for i being Nat
for a, b being Element of REAL n st 1 <= i & i < k & a = q0 /. i & b = p0 /. i holds
( q0 /. (i + 1) <> 0* n & q0 . (i + 1) = (q0 /. i) - (|(a,b)| * (p0 /. i)) ) by A16, A18;
reconsider a2 = q0 /. k, b2 = p0 /. k as Element of REAL n ;
reconsider q3 = <*((q0 /. k) - (|(a2,b2)| * (p0 /. k)))*> as FinSequence of REAL n ;
reconsider q1 = q0 ^ q3 as FinSequence of REAL n ;
1 in Seg (len q0) by A20, A21, FINSEQ_1:1;
then A25: 1 in dom q0 by FINSEQ_1:def 3;
then A26: q1 . 1 = z0 by A23, FINSEQ_1:def 7;
A27: 1 <= k + 1 by NAT_1:12;
A28: ( k + 1 <= len p implies p0 /. (k + 1) in B )

proof

assume A29: k + 1 <= len p ; :: thesis:
then k + 1 in dom p by A27, FINSEQ_3:25;
then p . (k + 1) in rng p by FUNCT_1:def 3;
hence p0 /. (k + 1) in B by A11, A29, FINSEQ_4:15, NAT_1:12; :: thesis:

end;

A30: len q1 = (len q0) + (len q3) by FINSEQ_1:22
.= k + 1 by A20, FINSEQ_1:40 ;
A31: for i being Nat
for a, b being Element of REAL n st 1 <= i & i < k + 1 & a = q1 /. i & b = p0 /. i holds
( q1 /. (i + 1) <> 0* n & q1 . (i + 1) = (q1 /. i) - (|(a,b)| * (p0 /. i)) )

proof

let i be Nat; :: thesis:
let a, b be Element of REAL n; :: thesis:
assume that
A32: 1 <= i and
A33: i < k + 1 and
A34: a = q1 /. i and
A35: b = p0 /. i ; :: thesis:
A36: i <= k by A33, NAT_1:13;
A37: i + 1 <= k + 1 by A33, NAT_1:13;
A38: 1 <= i + 1 by NAT_1:12;

per cases by A36, XXREAL_0:1;

suppose A39: i < k ; :: thesis:

then A40: i + 1 <= k by NAT_1:13;
then A41: q1 . (i + 1) = q0 . (i + 1) by A20, FINSEQ_1:64, NAT_1:12;
A42: q1 /. (i + 1) = q1 . (i + 1) by A30, A38, A37, FINSEQ_4:15;
A43: q0 /. (i + 1) = q0 . (i + 1) by A20, A40, FINSEQ_4:15, NAT_1:12;
q1 /. i = q1 . i by A30, A32, A33, FINSEQ_4:15
.= q0 . i by A20, A32, A36, FINSEQ_1:64
.= q0 /. i by A20, A32, A36, FINSEQ_4:15 ;
hence ( q1 /. (i + 1) <> 0* n & q1 . (i + 1) = (q1 /. i) - (|(a,b)| * (p0 /. i)) ) by A24, A32, A34, A35, A39, A41, A42, A43; :: thesis:

end;

suppose A44: i = k ; :: thesis:

then A45: q1 /. (i + 1) = q1 . (k + 1) by A30, A27, FINSEQ_4:15
.= q3 . ((k + 1) - (len q0)) by A20, A30, FINSEQ_1:24, XREAL_1:29
.= (q0 /. k) - (|(a2,b2)| * (p0 /. k)) by A20, FINSEQ_1:40 ;

A46: now

assume q1 /. (i + 1) = 0* n ; :: thesis:
then ((q0 /. k) - (|(a2,b2)| * (p0 /. k))) + (|(a2,b2)| * (p0 /. k)) = |(a2,b2)| * (p0 /. k) by A45, EUCLID_4:1;
then A47: q0 /. k = |(a2,b2)| * (p0 /. k) by RVSUM_1:43;
q0 /. k = q0 . k by A20, A21, FINSEQ_4:15;
hence contradiction by A17, A22, A47, XREAL_1:6; :: thesis:

end;

k < k + 1 by XREAL_1:29;
then A48: q1 /. k = q1 . k by A21, A30, FINSEQ_4:15;
A49: q0 /. k = q0 . k by A20, A21, FINSEQ_4:15;
q1 . k = q0 . k by A20, A21, FINSEQ_1:64;
hence ( q1 /. (i + 1) <> 0* n & q1 . (i + 1) = (q1 /. i) - (|(a,b)| * (p0 /. i)) ) by A30, A34, A35, A38, A44, A49, A48, A45, A46, FINSEQ_4:15; :: thesis:

end;

A50: for s1 being Element of (RealVectSpace (Seg n))
for a01 being Real st s1 in B holds
a01 * s1 in the carrier of (Lin B)

proof

let s1 be Element of (RealVectSpace (Seg n)); :: thesis:
let a01 be Real; :: thesis:
assume A51: s1 in B ; :: thesis:
{s1} c= B

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in {s1} ; :: thesis:
hence z in B by A51, TARSKI:def 1; :: thesis:

end;

then Lin {s1} is Subspace of Lin B by RLVECT_3:20;
then A52: the carrier of (Lin {s1}) c= the carrier of (Lin B) by RLSUB_1:def 2;
a01 * s1 in Lin {s1} by RLVECT_4:8;
then a01 * s1 in the carrier of (Lin {s1}) by STRUCT_0:def 5;
hence a01 * s1 in the carrier of (Lin B) by A52; :: thesis:

end;

A53: for s1 being Element of REAL n
for a01 being Real st s1 in B holds
a01 * s1 in the carrier of (Lin B)

proof

let s1 be Element of REAL n; :: thesis:
let a01 be Real; :: thesis:
reconsider s10 = s1 as Element of (RealVectSpace (Seg n)) by FINSEQ_2:93;
A54: a01 * s1 = a01 * s10 ;
assume s1 in B ; :: thesis:
hence a01 * s1 in the carrier of (Lin B) by A50, A54; :: thesis:

end;

defpred S₂[ Nat] means ( $1 + 1 <= k + 1 implies not q1 . ($1 + 1) in the carrier of (Lin B) );
A55: for j being Nat st S₂[j] holds
S₂[j + 1]

proof

let j be Nat; :: thesis:
assume A56: S₂[j] ; :: thesis:
( (j + 1) + 1 <= k + 1 implies not q1 . ((j + 1) + 1) in the carrier of (Lin B) )

proof

A57: B c= the carrier of (Lin B)

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in B ; :: thesis:
then z in Lin B by RLVECT_3:15;
hence z in the carrier of (Lin B) by STRUCT_0:def 5; :: thesis:

end;

assume (j + 1) + 1 <= k + 1 ; :: thesis:
then A58: j + 1 <= k by XREAL_1:6;

per cases by A58, XXREAL_0:1;

suppose A59: j + 1 = k ; :: thesis:

1 <= j + 1 by NAT_1:12;
then j + 1 in dom p0 by A19, A59, FINSEQ_3:25;
then A60: p0 . (j + 1) in rng p by FUNCT_1:def 3;
A61: p0 /. (j + 1) = p0 . (j + 1) by A19, A59, FINSEQ_4:15, NAT_1:12;
1 <= (j + 1) + 1 by NAT_1:12;
then A62: q1 /. ((j + 1) + 1) = q1 . ((j + 1) + 1) by A30, A59, FINSEQ_4:15;
A63: q1 . ((j + 1) + 1) = (q0 /. k) - (|(a2,b2)| * (p0 /. k)) by A20, A59, FINSEQ_1:42;

now

assume A64: q1 . ((j + 1) + 1) in the carrier of (Lin B) ; :: thesis:
(q1 /. ((j + 1) + 1)) + (|(a2,b2)| * (p0 /. (j + 1))) = q0 /. (j + 1) by A59, A63, A62, RVSUM_1:43;
then q0 /. (j + 1) in the carrier of (Lin B) by A11, A57, A62, A60, A61, A64, Lm3;
then A65: q0 /. (j + 1) in Lin B by STRUCT_0:def 5;
A66: not q1 . (j + 1) in Lin B by A56, A59, STRUCT_0:def 5, XREAL_1:29;
q1 . (j + 1) = q0 . (j + 1) by A20, A21, A59, FINSEQ_1:64;
hence contradiction by A20, A21, A59, A65, A66, FINSEQ_4:15; :: thesis:

end;

hence not q1 . ((j + 1) + 1) in the carrier of (Lin B) ; :: thesis:

end;

suppose A67: j + 1 < k ; :: thesis:

reconsider a11 = q0 /. (j + 1), b11 = p0 /. (j + 1) as Element of REAL n ;
A68: (j + 1) + 1 <= k by A67, NAT_1:13;
then A69: q0 /. ((j + 1) + 1) = q0 . ((j + 1) + 1) by A20, FINSEQ_4:15, NAT_1:12;
A70: j + 1 <= len p0 by A19, A67, XXREAL_0:2;
then A71: p0 /. (j + 1) = p0 . (j + 1) by FINSEQ_4:15, NAT_1:12;
A72: 1 <= j + 1 by NAT_1:12;
then j + 1 in dom p0 by A70, FINSEQ_3:25;
then A73: p0 . (j + 1) in rng p by FUNCT_1:def 3;
A74: q1 . ((j + 1) + 1) = q0 . ((j + 1) + 1) by A20, A68, FINSEQ_1:64, NAT_1:12;
A75: q0 . ((j + 1) + 1) = (q0 /. (j + 1)) - (|(a11,b11)| * (p0 /. (j + 1))) by A24, A67, A72;

now

assume A76: q1 . ((j + 1) + 1) in the carrier of (Lin B) ; :: thesis:
(q0 /. ((j + 1) + 1)) + (|(a11,b11)| * (p0 /. (j + 1))) = q0 /. (j + 1) by A75, A69, RVSUM_1:43;
then q0 /. (j + 1) in the carrier of (Lin B) by A11, A57, A69, A73, A71, A74, A76, Lm3;
then A77: q0 /. (j + 1) in Lin B by STRUCT_0:def 5;
k < k + 1 by XREAL_1:29;
then A78: not q1 . (j + 1) in Lin B by A56, A67, STRUCT_0:def 5, XXREAL_0:2;
q1 . (j + 1) = q0 . (j + 1) by A20, A67, FINSEQ_1:64, NAT_1:12;
hence contradiction by A20, A67, A77, A78, FINSEQ_4:15, NAT_1:12; :: thesis:

end;

hence not q1 . ((j + 1) + 1) in the carrier of (Lin B) ; :: thesis:

end;

hence S₂[j + 1] ; :: thesis:

end;

A79: S₂[ 0 ] by A9, A23, A25, FINSEQ_1:def 7;
for j being Nat holds S₂[j] from NAT_1:sch 2(A79, A55);
then ( k + 1 <= len p implies for d being Real holds not q1 . (k + 1) = d * (p0 /. (k + 1)) ) by A53, A28;
hence S₁[k + 1] by A30, A26, A31; :: thesis:

end;

suppose A80: 1 > k ; :: thesis:

reconsider q1 = <*z0*> as FinSequence of REAL n ;
A81: len q1 = 1 by FINSEQ_1:40;
A82: q1 . 1 = z0 by FINSEQ_1:40;
A83: ( 1 <= len p implies for d being Real holds not q1 . 1 = d * (p0 /. 1) )

proof

assume A84: 1 <= len p ; :: thesis:
thus for d being Real holds not q1 . 1 = d * (p0 /. 1) :: thesis:

proof

let d be Real; :: thesis:
A85: q1 . 1 = z0 by FINSEQ_1:40;
1 in dom p0 by A84, FINSEQ_3:25;
then A86: p0 . 1 in B by A11, FUNCT_1:def 3;
p0 /. 1 = p0 . 1 by A84, FINSEQ_4:15;
hence not q1 . 1 = d * (p0 /. 1) by A3, A8, A10, A14, A85, A86, Th43; :: thesis:

end;

A87: for i being Nat
for a, b being Element of REAL n st 1 <= i & i < 1 & a = q1 /. i & b = p0 /. i holds
( q1 /. (i + 1) <> 0* n & q1 . (i + 1) = (q1 /. i) - (|(a,b)| * (p0 /. i)) ) ;
k = 0 by A80, NAT_1:14;
hence S₁[k + 1] by A81, A82, A83, A87; :: thesis:

end;

suppose ( not 1 <= k + 1 or not k + 1 <= (len p) + 1 ) ; :: thesis:

hence S₁[k + 1] ; :: thesis:

end;

A88: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A88, A15);
then consider q being FinSequence of REAL n such that
A89: len q = (len p) + 1 and
( (len p) + 1 <= len p implies for d being Real holds not q . ((len p) + 1) = d * (p0 /. ((len p) + 1)) ) and
q . 1 = z0 and
A90: for i being Nat
for a, b being Element of REAL n st 1 <= i & i < (len p) + 1 & a = q /. i & b = p0 /. i holds
( q /. (i + 1) <> 0* n & q . (i + 1) = (q /. i) - (|(a,b)| * (p0 /. i)) ) by A13;
reconsider u4 = q /. (len q) as Element of REAL n ;
A91: len p < (len p) + 1 by XREAL_1:29;
set u0 = (1 / |.u4.|) * u4;
reconsider B3 = B \/ {((1 / |.u4.|) * u4)} as Subset of (REAL n) by XBOOLE_1:8;
A92: for i being Nat
for s being Element of REAL n st 1 <= i & i <= len p & p0 /. i = s holds
|(s,u4)| = 0

proof

defpred S₂[ Nat] means for s2, u2 being Element of REAL n
for k being Nat st u2 = q /. $1 & 1 <= k & k < $1 & $1 <= (len p) + 1 & p0 /. k = s2 holds
|(s2,u2)| = 0 ;
let i be Nat; :: thesis:
let s be Element of REAL n; :: thesis:
assume that
A93: 1 <= i and
A94: i <= len p and
A95: p0 /. i = s ; :: thesis:
A96: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis:
assume A97: S₂[k] ; :: thesis:
for s2, u2 being Element of REAL n
for k2 being Nat st u2 = q /. (k + 1) & 1 <= k2 & k2 < k + 1 & k + 1 <= (len p) + 1 & p0 /. k2 = s2 holds
|(s2,u2)| = 0

proof

A98: k < k + 1 by XREAL_1:29;
let s2, u2 be Element of REAL n; :: thesis:
let k2 be Nat; :: thesis:
assume that
A99: u2 = q /. (k + 1) and
A100: 1 <= k2 and
A101: k2 < k + 1 and
A102: k + 1 <= (len p) + 1 and
A103: p0 /. k2 = s2 ; :: thesis:
A104: k2 <= k by A101, NAT_1:13;

per cases ;

suppose k = 0 ; :: thesis:

hence |(s2,u2)| = 0 by A100, A101; :: thesis:

end;

suppose A105: k <> 0 ; :: thesis:

reconsider a = q /. k, b = p0 /. k as Element of REAL n ;
A106: k < (len p) + 1 by A102, A98, XXREAL_0:2;
then A107: k <= len p by NAT_1:13;
1 <= k + 1 by A100, A101, XXREAL_0:2;
then A108: u2 = q . (k + 1) by A89, A99, A102, FINSEQ_4:15;
A109: 0 + 1 <= k by A105, NAT_1:13;
then q . (k + 1) = (q /. k) - (|(a,b)| * (p0 /. k)) by A90, A106;
then A110: |(s2,u2)| = |(s2,a)| - |(s2,(|(a,b)| * b))| by A108, EUCLID_4:26
.= |(s2,a)| - (|(a,b)| * |(s2,b)|) by EUCLID_4:21 ;

per cases by A104, XXREAL_0:1;

suppose A111: k2 < k ; :: thesis:

then A112: 1 < k by A100, XXREAL_0:2;
then A113: p0 /. k = p0 . k by A107, FINSEQ_4:15;
k in Seg (len p0) by A107, A112, FINSEQ_1:1;
then A114: k in dom p0 by FINSEQ_1:def 3;
then A115: b in D by A11, A113, FUNCT_1:def 3;
A116: k < (len p) + 1 by A102, A98, XXREAL_0:2;
A117: k2 < len p by A107, A111, XXREAL_0:2;
then A118: p0 /. k2 = p0 . k2 by A100, FINSEQ_4:15;
k2 in Seg (len p0) by A100, A117, FINSEQ_1:1;
then A119: k2 in dom p0 by FINSEQ_1:def 3;
then A120: s2 in rng p by A103, A118, FUNCT_1:def 3;
s2 <> b by A12, A103, A111, A118, A119, A113, A114, FUNCT_1:def 4;
then |(s2,b)| = 0 by A11, A120, A115, Def3;
hence |(s2,u2)| = 0 by A97, A100, A103, A110, A111, A116; :: thesis:

end;

suppose A121: k2 = k ; :: thesis:

k in Seg (len p0) by A109, A107, FINSEQ_1:1;
then A122: k in dom p0 by FINSEQ_1:def 3;
p0 /. k = p0 . k by A109, A107, FINSEQ_4:15;
then b in rng p0 by A122, FUNCT_1:def 3;
then |.b.| = 1 by A11, Def4;
then |.b.| ^2 = 1 ;
hence |(s2,u2)| = |(b,a)| - (|(a,b)| * 1) by A103, A110, A121, EUCLID_2:4
.= 0 ;
:: thesis:

end;

hence S₂[k + 1] ; :: thesis:

end;

A123: S₂[ 0 ] ;
A124: for k being Nat holds S₂[k] from NAT_1:sch 2(A123, A96);
len p < (len p) + 1 by XREAL_1:29;
then i < len q by A89, A94, XXREAL_0:2;
hence |(s,u4)| = 0 by A89, A93, A95, A124; :: thesis:

end;

A125: for i being Nat
for s being Element of REAL n st 1 <= i & i <= len p & p0 /. i = s holds
|(s,((1 / |.u4.|) * u4))| = 0

proof

let i be Nat; :: thesis:
let s be Element of REAL n; :: thesis:
assume that
A126: 1 <= i and
A127: i <= len p and
A128: p0 /. i = s ; :: thesis:
A129: |(s,((1 / |.u4.|) * u4))| = (1 / |.u4.|) * |(s,u4)| by EUCLID_4:22;
|(s,u4)| = 0 by A92, A126, A127, A128;
hence |(s,((1 / |.u4.|) * u4))| = 0 by A129; :: thesis:

end;

for x, y being real-valued FinSequence st x in B3 & y in B3 & x <> y holds
|(x,y)| = 0

proof

let x, y be real-valued FinSequence; :: thesis:
assume that
A130: x in B3 and
A131: y in B3 and
A132: x <> y ; :: thesis:

per cases by A130, A131, XBOOLE_0:def 3;

suppose ( x in B & y in B ) ; :: thesis:

hence |(x,y)| = 0 by A132, Def3; :: thesis:

end;

suppose A133: ( x in B & y in {((1 / |.u4.|) * u4)} ) ; :: thesis:

then consider x3 being set such that
A134: x3 in dom p0 and
A135: x = p0 . x3 by A11, FUNCT_1:def 3;
reconsider j = x3 as Element of NAT by A134;
A136: x3 in Seg (len p0) by A134, FINSEQ_1:def 3;
then A137: j <= len p0 by FINSEQ_1:1;
A138: y = (1 / |.u4.|) * u4 by A133, TARSKI:def 1;
A139: 1 <= j by A136, FINSEQ_1:1;
then p0 . x3 = p0 /. j by A137, FINSEQ_4:15;
hence |(x,y)| = 0 by A125, A138, A135, A139, A137; :: thesis:

end;

suppose A140: ( x in {((1 / |.u4.|) * u4)} & y in B ) ; :: thesis:

then consider y3 being set such that
A141: y3 in dom p0 and
A142: y = p0 . y3 by A11, FUNCT_1:def 3;
reconsider j = y3 as Element of NAT by A141;
A143: y3 in Seg (len p0) by A141, FINSEQ_1:def 3;
then A144: j <= len p0 by FINSEQ_1:1;
A145: x = (1 / |.u4.|) * u4 by A140, TARSKI:def 1;
A146: 1 <= j by A143, FINSEQ_1:1;
then p0 . y3 = p0 /. j by A144, FINSEQ_4:15;
hence |(x,y)| = 0 by A125, A145, A142, A146, A144; :: thesis:

end;

suppose A147: ( x in {((1 / |.u4.|) * u4)} & y in {((1 / |.u4.|) * u4)} ) ; :: thesis:

then y = (1 / |.u4.|) * u4 by TARSKI:def 1;
hence |(x,y)| = 0 by A132, A147, TARSKI:def 1; :: thesis:

end;

then A148: B3 is R-orthogonal by Def3;
1 in dom p by A2, A11, FINSEQ_3:32;
then A149: 1 <= len p by FINSEQ_3:25;
set aq = q /. (len p);
set bq = p0 /. (len p);
A150: p0 /. (len p) = p0 /. (len p) ;
q /. (len p) = q /. (len p) ;
then A151: |.u4.| <> 0 by A149, A89, A90, A150, A91, EUCLID:8;
A152: abs (1 / |.u4.|) = 1 / |.u4.| by ABSVALUE:def 1;
A153: (1 / |.u4.|) * u4 in {((1 / |.u4.|) * u4)} by TARSKI:def 1;
A154: |.((1 / |.u4.|) * u4).| = (abs (1 / |.u4.|)) * |.u4.| by EUCLID:11
.= 1 by A151, A152, XCMPLX_1:106 ;
then B3 is R-normal by Th18;
then D0 = B3 by A5, A148, XBOOLE_1:7;
then (1 / |.u4.|) * u4 in B by A153, XBOOLE_0:def 3;
then consider x3 being set such that
A155: x3 in dom p0 and
A156: (1 / |.u4.|) * u4 = p0 . x3 by A11, FUNCT_1:def 3;
reconsider j = x3 as Element of NAT by A155;
A157: x3 in Seg (len p0) by A155, FINSEQ_1:def 3;
then A158: j <= len p0 by FINSEQ_1:1;
A159: 1 <= j by A157, FINSEQ_1:1;
then p0 . x3 = p0 /. j by A158, FINSEQ_4:15;
then |(((1 / |.u4.|) * u4),((1 / |.u4.|) * u4))| = 0 by A125, A156, A159, A158;
hence B is Basis of RealVectSpace (Seg n) by A154, EUCLID_4:16; :: thesis:

end;

Lin B is Subspace of Lin I by A3, RLVECT_3:20;
then A160: the carrier of (Lin B) c= the carrier of (Lin I) by RLSUB_1:def 2;
A161: Lin I = RealVectSpace (Seg n) by RLVECT_3:def 3;

now

assume I c= the carrier of (Lin B) ; :: thesis:
then Lin I is Subspace of Lin B by RLVECT_5:19;
then the carrier of (Lin I) c= the carrier of (Lin B) by RLSUB_1:def 2;
then the carrier of (Lin I) = the carrier of (Lin B) by A160, XBOOLE_0:def 10;
then Lin B = Lin I by RLSUB_1:30;
hence B is Basis of RealVectSpace (Seg n) by A161, RLVECT_3:def 3; :: thesis:

end;

hence D is Basis of RealVectSpace (Seg n) by A6; :: thesis:

end;