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₁( 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₁(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