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 Th17, Th47; :: thesis:

end;

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

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

A5: now :: thesis:

assume that
B <> I and
A6: not I c= the carrier of (Lin B) ; :: thesis:
consider x0 being object such that
A7: x0 in I and
A8: not x0 in the carrier of (Lin B) by A6;
reconsider z0 = x0 as Element of REAL n by A7, FINSEQ_2:93;
not x0 in Lin B by A8;
then A9: not x0 in B by RLVECT_3:15;
consider p being FinSequence such that
A10: rng p = B and
A11: p is one-to-one by A2, A3, FINSEQ_4:58;
A12: 1 <= (len p) + 1 by NAT_1:12;
reconsider p0 = p as FinSequence of REAL n by A10, 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)) ) ) ) );
A13: I is linearly-independent by RLVECT_3:def 3;
A14: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

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

per cases ;

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

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

per cases ;

suppose 1 <= k ; :: thesis:

then consider q0 being FinSequence of REAL n such that
A19: len q0 = k and
A20: 1 <= k and
k <= (len p) + 1 and
A21: ( k <= len p implies for d being Real holds not q0 . k = d * (p0 /. k) ) and
A22: q0 . 1 = z0 and
A23: 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 A15, A17;
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 A19, A20, FINSEQ_1:1;
then A24: 1 in dom q0 by FINSEQ_1:def 3;
then A25: q1 . 1 = z0 by A22, FINSEQ_1:def 7;
A26: 1 <= k + 1 by NAT_1:12;
A27: ( k + 1 <= len p implies p0 /. (k + 1) in B )

proof

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

end;

A29: len q1 = (len q0) + (len q3) by FINSEQ_1:22
.= k + 1 by A19, FINSEQ_1:40 ;
A30: 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
A31: 1 <= i and
A32: i < k + 1 and
A33: a = q1 /. i and
A34: b = p0 /. i ; :: thesis:
A35: i <= k by A32, NAT_1:13;
A36: i + 1 <= k + 1 by A32, NAT_1:13;
A37: 1 <= i + 1 by NAT_1:12;

per cases by A35, XXREAL_0:1;

suppose A38: i < k ; :: thesis:

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

end;

suppose A43: i = k ; :: thesis:

then A44: q1 /. (i + 1) = q1 . (k + 1) by A29, A26, FINSEQ_4:15
.= q3 . ((k + 1) - (len q0)) by A19, A29, FINSEQ_1:24, XREAL_1:29
.= (q0 /. k) - (|(a2,b2)| * (p0 /. k)) by A19 ;

A45: now :: thesis:

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

end;

k < k + 1 by XREAL_1:29;
then A47: q1 /. k = q1 . k by A20, A29, FINSEQ_4:15;
A48: q0 /. k = q0 . k by A19, A20, FINSEQ_4:15;
q1 . k = q0 . k by A19, A20, FINSEQ_1:64;
hence ( q1 /. (i + 1) <> 0* n & q1 . (i + 1) = (q1 /. i) - (|(a,b)| * (p0 /. i)) ) by A29, A33, A34, A37, A43, A48, A47, A44, A45, FINSEQ_4:15; :: thesis:

end;

A49: 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 A50: s1 in B ; :: thesis:
{s1} c= B by A50, TARSKI:def 1;
then Lin {s1} is Subspace of Lin B by RLVECT_3:20;
then A51: 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}) ;
hence a01 * s1 in the carrier of (Lin B) by A51; :: thesis:

end;

A52: 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;
reconsider aa = a01 as Element of REAL by XREAL_0:def 1;
A53: aa * s1 = aa * s10 ;
assume s1 in B ; :: thesis:
hence a01 * s1 in the carrier of (Lin B) by A49, A53; :: thesis:

end;

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

proof

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

proof

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

proof

let z be object ; :: 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) ; :: thesis:

end;

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

per cases by A57, XXREAL_0:1;

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

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

now :: thesis:

assume A63: q1 . ((j + 1) + 1) in the carrier of (Lin B) ; :: thesis:
(q1 /. ((j + 1) + 1)) + (|(a2,b2)| * (p0 /. (j + 1))) = q0 /. (j + 1) by A58, A62, A61, RVSUM_1:43;
then q0 /. (j + 1) in the carrier of (Lin B) by A10, A56, A61, A59, A60, A63, Lm4;
then A64: q0 /. (j + 1) in Lin B ;
A65: not q1 . (j + 1) in Lin B by A55, A58, XREAL_1:29;
q1 . (j + 1) = q0 . (j + 1) by A19, A20, A58, FINSEQ_1:64;
hence contradiction by A19, A20, A58, A64, A65, FINSEQ_4:15; :: thesis:

end;

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

end;

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

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

now :: thesis:

assume A75: q1 . ((j + 1) + 1) in the carrier of (Lin B) ; :: thesis:
(q0 /. ((j + 1) + 1)) + (|(a11,b11)| * (p0 /. (j + 1))) = q0 /. (j + 1) by A74, A68, RVSUM_1:43;
then q0 /. (j + 1) in the carrier of (Lin B) by A10, A56, A68, A72, A70, A73, A75, Lm4;
then A76: q0 /. (j + 1) in Lin B ;
k < k + 1 by XREAL_1:29;
then A77: not q1 . (j + 1) in Lin B by A55, A66, XXREAL_0:2;
q1 . (j + 1) = q0 . (j + 1) by A19, A66, FINSEQ_1:64, NAT_1:12;
hence contradiction by A19, A66, A76, A77, 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;

A78: S₂[ 0 ] by A8, A22, A24, FINSEQ_1:def 7;
for j being Nat holds S₂[j] from NAT_1:sch 2(A78, A54);
then ( k + 1 <= len p implies for d being Real holds not q1 . (k + 1) = d * (p0 /. (k + 1)) ) by A52, A27;
hence S₁[k + 1] by A29, A25, A30; :: thesis:

end;

suppose A79: 1 > k ; :: thesis:

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

proof

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

proof

let d be Real; :: thesis:
1 in dom p0 by A83, FINSEQ_3:25;
then A85: p0 . 1 in B by A10, FUNCT_1:def 3;
p0 /. 1 = p0 . 1 by A83, FINSEQ_4:15;
hence not q1 . 1 = d * (p0 /. 1) by A2, A7, A9, A13, A85, Th39; :: thesis:

end;

A86: 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 A79, NAT_1:14;
hence S₁[k + 1] by A80, A81, A82, A86; :: thesis:

end;

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

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

end;

A87: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A87, A14);
then consider q being FinSequence of REAL n such that
A88: 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
A89: 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 A12;
reconsider u4 = q /. (len q) as Element of REAL n ;
A90: 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;
A91: 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
A92: 1 <= i and
A93: i <= len p and
A94: p0 /. i = s ; :: thesis:
A95: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis:
assume A96: 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

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

per cases ;

suppose k = 0 ; :: thesis:

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

end;

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

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

per cases by A103, XXREAL_0:1;

suppose A110: k2 < k ; :: thesis:

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

end;

suppose A120: k2 = k ; :: thesis:

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

end;

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

end;

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

end;

A124: 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
A125: 1 <= i and
A126: i <= len p and
A127: p0 /. i = s ; :: thesis:
A128: |(s,((1 / |.u4.|) * u4))| = (1 / |.u4.|) * |(s,u4)| by EUCLID_4:22;
|(s,u4)| = 0 by A91, A125, A126, A127;
hence |(s,((1 / |.u4.|) * u4))| = 0 by A128; :: 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
A129: x in B3 and
A130: y in B3 and
A131: x <> y ; :: thesis:

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

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

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

end;

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

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

end;

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

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

end;

suppose A146: ( 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 A131, A146, TARSKI:def 1; :: thesis:

end;

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

end;

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

now :: thesis:

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 A159, XBOOLE_0:def 10;
then Lin B = Lin I by RLSUB_1:30;
hence B is Basis of RealVectSpace (Seg n) by A160, RLVECT_3:def 3; :: thesis:

end;

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

end;