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 H1( 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 = H1(k) from 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 ;
assume ( 1 <= k & k <= len A ) ; :: thesis: A /. k = KL . (b1 /. k)
then A6: k in Seg (len b1) by ;
then k in dom A by ;
then A . k = A /. k by PARTFUN1:def 6;
hence A /. k = KL . (b1 /. k) by A4, A5, A6; :: thesis: verum