let F be Field; :: thesis:
let U be non trivial finite-dimensional VectSp of F; :: thesis:
let V be finite-dimensional VectSp of F; :: thesis:
let B be Basis of U; :: thesis:
let f be Function of B,V; :: thesis:
let l2 be Linear_Combination of rng f; :: thesis:
set T = canLinTrans f;
defpred S₁[ Nat] means for l2 being Linear_Combination of rng f st card (Carrier l2) = $1 holds
ex l1 being Linear_Combination of B st (canLinTrans f) . (Sum l1) = Sum l2;
IA: S₁[ 0 ]

proof

now :: thesis:

let l2 be Linear_Combination of rng f; :: thesis:
assume card (Carrier l2) = 0 ; :: thesis:
then Carrier l2 = {} ;
then l2 = ZeroLC V by VECTSP_6:def 3;
then A3: Sum l2 = 0. V by VECTSP_6:15;
Carrier (ZeroLC U) c= B by VECTSP_6:def 3;
then reconsider l1 = ZeroLC U as Linear_Combination of B by VECTSP_6:def 4;
Sum l1 = 0. U by VECTSP_6:15;
then (canLinTrans f) . (Sum l1) = Sum l2 by A3, RANKNULL:9;
hence ex l1 being Linear_Combination of B st (canLinTrans f) . (Sum l1) = Sum l2 ; :: thesis:

end;

hence S₁[ 0 ] ; :: thesis:

end;

I1: S₁[1]

proof

now :: thesis:

let l2 be Linear_Combination of rng f; :: thesis:
assume card (Carrier l2) = 1 ; :: thesis:
then consider v being object such that
A2: Carrier l2 = {v} by CARD_2:42;
A3: ( Carrier l2 c= rng f & v in Carrier l2 ) by A2, TARSKI:def 1, VECTSP_6:def 4;
then reconsider v = v as Element of V ;
consider u being object such that
A4: ( u in dom f & f . u = v ) by A3, FUNCT_1:def 3;
reconsider u = u as Element of B by A4;
A5: (canLinTrans f) . u = ((canLinTrans f) | B) . u by FUNCT_1:49
.= f . u by defcl ;
defpred S₂[ object , object ] means ( ( $1 = u & $2 = l2 . (f . u) ) or ( $1 <> u & $2 = 0. F ) );
B4: for x being object st x in the carrier of U holds
ex y being object st
( y in the carrier of F & S₂[x,y] )

proof

let x be object ; :: thesis:
assume x in the carrier of U ; :: thesis:

per cases ;

suppose x = u ; :: thesis:

hence ex y being object st
( y in the carrier of F & S₂[x,y] ) ; :: thesis:

end;

suppose x <> u ; :: thesis:

hence ex y being object st
( y in the carrier of F & S₂[x,y] ) ; :: thesis:

end;

consider l1 being Function of the carrier of U, the carrier of F such that
B5: for x being object st x in the carrier of U holds
S₂[x,l1 . x] from FUNCT_2:sch 1(B4);
reconsider l1 = l1 as Element of Funcs ( the carrier of U, the carrier of F) by FUNCT_2:8;
H: {u} c= the carrier of U by TARSKI:def 3;
for v being Element of U st not v in {u} holds
l1 . v = 0. F

proof

let v be Element of U; :: thesis:
assume not v in {u} ; :: thesis:
then v <> u by TARSKI:def 1;
hence l1 . v = 0. F by B5; :: thesis:

end;

then reconsider l1 = l1 as Linear_Combination of U by H, VECTSP_6:def 1;

now :: thesis:

let o be object ; :: thesis:
assume o in Carrier l1 ; :: thesis:
then consider w being Element of U such that
C1: ( o = w & l1 . w <> 0. F ) ;
S₂[w,l1 . w] by B5;
hence o in {u} by C1, TARSKI:def 1; :: thesis:

end;

then B6: Carrier l1 c= {u} ;

now :: thesis:

let o be object ; :: thesis:
assume o in Carrier l1 ; :: thesis:
then o = u by B6, TARSKI:def 1;
hence o in B ; :: thesis:

end;

then Carrier l1 c= B ;
then reconsider l1 = l1 as Linear_Combination of B by VECTSP_6:def 4;
Carrier l1 = {u}

proof

now :: thesis:

let o be object ; :: thesis:
assume o in {u} ; :: thesis:
then H: o = u by TARSKI:def 1;
B9: l1 . u = l2 . v by A4, B5;
v in Carrier l2 by A2, TARSKI:def 1;
then l2 . v <> 0. F by VECTSP_6:2;
hence o in Carrier l1 by H, B9; :: thesis:

end;

then {u} c= Carrier l1 ;
hence Carrier l1 = {u} by B6; :: thesis:

end;

then (canLinTrans f) . (Sum l1) = (canLinTrans f) . ((l1 . u) * u) by VECTSP_6:20
.= (l1 . u) * ((canLinTrans f) . u) by MOD_2:def 2
.= (l2 . v) * (f . u) by A5, B5, A4
.= Sum l2 by A4, A2, VECTSP_6:20 ;
hence ex l1 being Linear_Combination of B st (canLinTrans f) . (Sum l1) = Sum l2 ; :: thesis:

end;

hence S₁[1] ; :: thesis:

end;

IS: now :: thesis:

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

now :: thesis:

let l2 be Linear_Combination of rng f; :: thesis:
assume B1: card (Carrier l2) = k + 1 ; :: thesis:
then Carrier l2 <> {} ;
then consider o being object such that
B2: o in Carrier l2 by XBOOLE_0:def 1;
consider v being Element of V such that
B3: ( o = v & l2 . v <> 0. F ) by B2;
defpred S₂[ object , object ] means ( ( $1 = v & $2 = l2 . v ) or ( $1 <> v & $2 = 0. F ) );
B4: for x being object st x in the carrier of V holds
ex y being object st
( y in the carrier of F & S₂[x,y] )

proof

let x be object ; :: thesis:
assume x in the carrier of V ; :: thesis:

per cases ;

suppose x = v ; :: thesis:

hence ex y being object st
( y in the carrier of F & S₂[x,y] ) ; :: thesis:

end;

suppose x <> v ; :: thesis:

hence ex y being object st
( y in the carrier of F & S₂[x,y] ) ; :: thesis:

end;

consider l3 being Function of the carrier of V, the carrier of F such that
B5: for x being object st x in the carrier of V holds
S₂[x,l3 . x] from FUNCT_2:sch 1(B4);
reconsider l3 = l3 as Element of Funcs ( the carrier of V, the carrier of F) by FUNCT_2:8;
for w being Element of V st not w in {v} holds
l3 . w = 0. F

proof

let w be Element of V; :: thesis:
assume not w in {v} ; :: thesis:
then v <> w by TARSKI:def 1;
hence l3 . w = 0. F by B5; :: thesis:

end;

then reconsider l3 = l3 as Linear_Combination of V by VECTSP_6:def 1;

now :: thesis:

let o be object ; :: thesis:
assume o in Carrier l3 ; :: thesis:
then consider w being Element of V such that
C1: ( o = w & l3 . w <> 0. F ) ;
w = v by C1, B5;
hence o in {v} by C1, TARSKI:def 1; :: thesis:

end;

then B6: Carrier l3 c= {v} ;

now :: thesis:

let o be object ; :: thesis:
assume o in Carrier l3 ; :: thesis:
then o = v by B6, TARSKI:def 1;
then C1: o in Carrier l2 by B3;
Carrier l2 c= rng f by VECTSP_6:def 4;
hence o in rng f by C1; :: thesis:

end;

then Carrier l3 c= rng f ;
then reconsider l3 = l3 as Linear_Combination of rng f by VECTSP_6:def 4;
B8: Carrier l3 = {v}

proof

now :: thesis:

let o be object ; :: thesis:
assume C1: o in {v} ; :: thesis:
then o = v by TARSKI:def 1;
then l3 . o <> 0. F by B5, B3;
hence o in Carrier l3 by C1; :: thesis:

end;

then {v} c= Carrier l3 ;
hence Carrier l3 = {v} by B6; :: thesis:

end;

reconsider l4 = l2 - l3 as Linear_Combination of rng f by VECTSP_6:42;
C0: l4 + l3 = l2 + ((- l3) + l3) by VECTSP_6:26
.= l2 + (l3 - l3) by VECTSP_6:25
.= l2 + (ZeroLC V) by VECTSP_6:43
.= l2 by VECTSP_6:27 ;
C1: Carrier l4 = (Carrier l2) \ (Carrier l3)

proof

C4: now :: thesis:

let o be object ; :: thesis:
assume o in Carrier l4 ; :: thesis:
then consider w being Element of V such that
C5: ( o = w & l4 . w <> 0. F ) ;

C6: now :: thesis:

assume C7: v = w ; :: thesis:
l4 . w = (l2 . w) - (l3 . w) by VECTSP_6:40
.= (l2 . w) - (l2 . w) by B5, C7 ;
hence contradiction by C5, RLVECT_1:15; :: thesis:

end;

then C7: not w in Carrier l3 by B8, TARSKI:def 1;
l4 . w = (l2 . w) - (l3 . w) by VECTSP_6:40
.= (l2 . w) - (0. F) by C6, B5 ;
then w in Carrier l2 by C5;
hence o in (Carrier l2) \ (Carrier l3) by C5, C7, XBOOLE_0:def 5; :: thesis:

end;

now :: thesis:

let o be object ; :: thesis:
assume o in (Carrier l2) \ (Carrier l3) ; :: thesis:
then C5: ( o in Carrier l2 & not o in Carrier l3 ) by XBOOLE_0:def 5;
then consider w being Element of V such that
C6: ( o = w & l2 . w <> 0. F ) ;
l4 . w = (l2 . w) - (l3 . w) by VECTSP_6:40
.= (l2 . w) - (0. F) by C6, C5 ;
hence o in Carrier l4 by C6; :: thesis:

end;

hence Carrier l4 = (Carrier l2) \ (Carrier l3) by C4, TARSKI:2; :: thesis:

end;

now :: thesis:

let o be object ; :: thesis:
assume o in Carrier l3 ; :: thesis:
then C4: o = v by B8, TARSKI:def 1;
v in Carrier l3 by B8, TARSKI:def 1;
then C5: l3 . v <> 0. F by VECTSP_6:2;
l2 . v = l3 . v by B5;
hence o in Carrier l2 by C4, C5; :: thesis:

end;

then Carrier l3 c= Carrier l2 ;
then card ((Carrier l2) \ (Carrier l3)) = (card (Carrier l2)) - (card (Carrier l3)) by CARD_2:44
.= (k + 1) - 1 by B1, B8, CARD_2:42 ;
then consider l5 being Linear_Combination of B such that
C2: (canLinTrans f) . (Sum l5) = Sum l4 by IV, C1;
card (Carrier l3) = 1 by B8, CARD_1:30;
then consider l6 being Linear_Combination of B such that
C3: (canLinTrans f) . (Sum l6) = Sum l3 by I1;
reconsider l1 = l5 + l6 as Linear_Combination of B by VECTSP_6:24;
Sum l1 = (Sum l5) + (Sum l6) by VECTSP_6:44;
then (canLinTrans f) . (Sum l1) = ((canLinTrans f) . (Sum l5)) + ((canLinTrans f) . (Sum l6)) by VECTSP_1:def 20
.= Sum l2 by C0, C2, C3, VECTSP_6:44 ;
hence ex l1 being Linear_Combination of B st (canLinTrans f) . (Sum l1) = Sum l2 ; :: thesis:

end;

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

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 2(IA, IS);
consider n being Nat such that
H: card (Carrier l2) = n ;
thus ex l1 being Linear_Combination of B st (canLinTrans f) . (Sum l1) = Sum l2 by H, I; :: thesis: