let V1 be free finite-rank Z_Module; :: thesis: for b1 being OrdBasis of V1
for d being FinSequence of INT.Ring st len d = len b1 holds
d = (Sum (lmlt (d,b1))) |-- b1
let b1 be OrdBasis of V1; :: thesis: for d being FinSequence of INT.Ring st len d = len b1 holds
d = (Sum (lmlt (d,b1))) |-- b1
let d be FinSequence of INT.Ring; :: thesis: ( len d = len b1 implies d = (Sum (lmlt (d,b1))) |-- b1 )
reconsider T = rng b1 as finite Subset of V1 ;
defpred S₁[ Element of V1, Element of INT.Ring] means ( ( $1 in rng b1 implies for k being Nat st k in dom b1 & b1 /. k = $1 holds
$2 = d /. k ) & ( not $1 in rng b1 implies $2 = 0. INT.Ring ) );
A1: for v being Element of V1 ex u being Element of INT.Ring st S₁[v,u]

proof

let v be Element of V1; :: thesis: ex u being Element of INT.Ring st S₁[v,u]

per cases ( v in rng b1 or not v in rng b1 ) ;

suppose A2: v in rng b1 ; :: thesis: ex u being Element of INT.Ring st S₁[v,u]

then consider k being Element of NAT such that
A3: k in dom b1 and
A4: b1 /. k = v by PARTFUN2:2;
take u = d /. k; :: thesis: S₁[v,u]

now :: thesis: for i being Nat st i in dom b1 & b1 /. i = v holds
u = d /. i

A5: b1 is one-to-one by defOrdBasis;
let i be Nat; :: thesis: ( i in dom b1 & b1 /. i = v implies u = d /. i )
assume that
A6: i in dom b1 and
A7: b1 /. i = v ; :: thesis: u = d /. i
b1 . i = b1 /. k by A4, A6, A7, PARTFUN1:def 6
.= b1 . k by A3, PARTFUN1:def 6 ;
hence u = d /. i by A3, A6, A5; :: thesis: verum

end;

hence S₁[v,u] by A2; :: thesis: verum

end;

suppose A8: not v in rng b1 ; :: thesis: ex u being Element of INT.Ring st S₁[v,u]

reconsider I0 = 0. INT.Ring as Element of INT.Ring ;
take I0 ; :: thesis: S₁[v,I0]
thus S₁[v,I0] by A8; :: thesis: verum

end;

end;

end;

consider KL being Function of V1, the carrier of INT.Ring such that
A9: for v being Element of V1 holds S₁[v,KL . v] from FUNCT_2:sch 3(A1);

now :: thesis: ex f being Function of V1, the carrier of INT.Ring st
( KL = f & dom f = the carrier of V1 & rng f c= the carrier of INT.Ring )

take f = KL; :: thesis: ( KL = f & dom f = the carrier of V1 & rng f c= the carrier of INT.Ring )
thus ( KL = f & dom f = the carrier of V1 & rng f c= the carrier of INT.Ring ) by FUNCT_2:def 1; :: thesis: verum

end;

then KL in Funcs ( the carrier of V1, the carrier of INT.Ring) by FUNCT_2:def 2;
then reconsider KL1 = KL as Linear_Combination of V1 by A9, VECTSP_6:def 1;
assume A11: len d = len b1 ; :: thesis: d = (Sum (lmlt (d,b1))) |-- b1

now :: thesis: ex KL1 being Linear_Combination of V1 st
( ( for k being Nat st 1 <= k & k <= len d holds
d /. k = KL1 . (b1 /. k) ) & Carrier KL1 c= rng b1 & Sum (lmlt (d,b1)) = Sum KL1 )

take KL1 = KL1; :: thesis: ( ( for k being Nat st 1 <= k & k <= len d holds
d /. k = KL1 . (b1 /. k) ) & Carrier KL1 c= rng b1 & Sum (lmlt (d,b1)) = Sum KL1 )
thus A13: for k being Nat st 1 <= k & k <= len d holds
d /. k = KL1 . (b1 /. k) :: thesis: ( Carrier KL1 c= rng b1 & Sum (lmlt (d,b1)) = Sum KL1 )

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len d implies d /. k = KL1 . (b1 /. k) )
assume A141: ( 1 <= k & k <= len d ) ; :: thesis: d /. k = KL1 . (b1 /. k)
then A14: k in dom b1 by A11, FINSEQ_3:25;
then b1 . k = b1 /. k by PARTFUN1:def 6;
then b1 /. k in rng b1 by A14, FUNCT_1:def 3;
hence d /. k = KL1 . (b1 /. k) by A9, A11, A141, FINSEQ_3:25; :: thesis: verum

end;

for x being object st x in Carrier KL1 holds
x in rng b1

proof

let x be object ; :: thesis: ( x in Carrier KL1 implies x in rng b1 )
assume x in Carrier KL1 ; :: thesis: x in rng b1
then A15: ex v being Element of V1 st
( x = v & KL1 . v <> 0 ) ;
assume not x in rng b1 ; :: thesis: contradiction
hence contradiction by A9, A15; :: thesis: verum

end;

hence A16: Carrier KL1 c= rng b1 ; :: thesis: Sum (lmlt (d,b1)) = Sum KL1
A17: dom d = dom b1 by A11, FINSEQ_3:29;
then A18: dom (lmlt (d,b1)) = dom b1 by Th12;
then A19: len (lmlt (d,b1)) = len b1 by FINSEQ_3:29
.= len (KL1 (#) b1) by VECTSP_6:def 5 ;

now :: thesis: for k being Nat st k in dom (lmlt (d,b1)) holds
(lmlt (d,b1)) . k = (KL1 (#) b1) . k

let k be Nat; :: thesis: ( k in dom (lmlt (d,b1)) implies (lmlt (d,b1)) . k = (KL1 (#) b1) . k )
assume A20: k in dom (lmlt (d,b1)) ; :: thesis: (lmlt (d,b1)) . k = (KL1 (#) b1) . k
then A21: k in dom (KL1 (#) b1) by A19, FINSEQ_3:29;
A22: ( 1 <= k & k <= len d ) by A11, A18, A20, FINSEQ_3:25;
A23: ( d /. k = d . k & b1 /. k = b1 . k ) by A17, A18, A20, PARTFUN1:def 6;
thus (lmlt (d,b1)) . k = the lmult of V1 . ((d . k),(b1 . k)) by A20, FUNCOP_1:22
.= (KL1 . (b1 /. k)) * (b1 /. k) by A13, A22, A23
.= (KL1 (#) b1) . k by A21, VECTSP_6:def 5 ; :: thesis: verum

end;

hence Sum (lmlt (d,b1)) = Sum (KL1 (#) b1) by A19, FINSEQ_2:9
.= Sum KL1 by A16, defOrdBasis, Th20 ;
:: thesis: verum

end;

hence d = (Sum (lmlt (d,b1))) |-- b1 by A11, Def7; :: thesis: verum