reconsider b2 = rng b1 as Basis of V by Def2;

consider KL being Linear_Combination of V such that

A1: W = Sum KL and

A2: Carrier KL c= b2 by Th8;

deffunc H_{1}( Nat) -> Element of the carrier of K = KL . (b1 /. $1);

consider A being FinSequence of K such that

A3: len A = len b1 and

A4: for k being Nat st k in dom A holds

A . k = H_{1}(k)
from FINSEQ_2:sch 1();

take A ; :: thesis: ( len A = len b1 & ex KL being Linear_Combination of V st

( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len A holds

A /. k = KL . (b1 /. k) ) ) )

thus len A = len b1 by A3; :: thesis: ex KL being Linear_Combination of V st

( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len A holds

A /. k = KL . (b1 /. k) ) )

take KL ; :: thesis: ( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len A holds

A /. k = KL . (b1 /. k) ) )

thus W = Sum KL by A1; :: thesis: ( Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len A holds

A /. k = KL . (b1 /. k) ) )

thus Carrier KL c= rng b1 by A2; :: thesis: for k being Nat st 1 <= k & k <= len A holds

A /. k = KL . (b1 /. k)

let k be Nat; :: thesis: ( 1 <= k & k <= len A implies A /. k = KL . (b1 /. k) )

A5: dom A = Seg (len b1) by A3, FINSEQ_1:def 3;

assume ( 1 <= k & k <= len A ) ; :: thesis: A /. k = KL . (b1 /. k)

then A6: k in Seg (len b1) by A3, FINSEQ_1:1;

then k in dom A by A3, FINSEQ_1:def 3;

then A . k = A /. k by PARTFUN1:def 6;

hence A /. k = KL . (b1 /. k) by A4, A5, A6; :: thesis: verum

consider KL being Linear_Combination of V such that

A1: W = Sum KL and

A2: Carrier KL c= b2 by Th8;

deffunc H

consider A being FinSequence of K such that

A3: len A = len b1 and

A4: for k being Nat st k in dom A holds

A . k = H

take A ; :: thesis: ( len A = len b1 & ex KL being Linear_Combination of V st

( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len A holds

A /. k = KL . (b1 /. k) ) ) )

thus len A = len b1 by A3; :: thesis: ex KL being Linear_Combination of V st

( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len A holds

A /. k = KL . (b1 /. k) ) )

take KL ; :: thesis: ( W = Sum KL & Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len A holds

A /. k = KL . (b1 /. k) ) )

thus W = Sum KL by A1; :: thesis: ( Carrier KL c= rng b1 & ( for k being Nat st 1 <= k & k <= len A holds

A /. k = KL . (b1 /. k) ) )

thus Carrier KL c= rng b1 by A2; :: thesis: for k being Nat st 1 <= k & k <= len A holds

A /. k = KL . (b1 /. k)

let k be Nat; :: thesis: ( 1 <= k & k <= len A implies A /. k = KL . (b1 /. k) )

A5: dom A = Seg (len b1) by A3, FINSEQ_1:def 3;

assume ( 1 <= k & k <= len A ) ; :: thesis: A /. k = KL . (b1 /. k)

then A6: k in Seg (len b1) by A3, FINSEQ_1:1;

then k in dom A by A3, FINSEQ_1:def 3;

then A . k = A /. k by PARTFUN1:def 6;

hence A /. k = KL . (b1 /. k) by A4, A5, A6; :: thesis: verum