let F be Field; :: thesis:
let U, V be VectSp of F; :: thesis:
let B be Subset of U; :: thesis:
let A be Subset of V; :: thesis:
let T be linear-transformation of U,V; :: thesis:
assume AS: T .: B c= A ; :: thesis:
let l be Linear_Combination of B; :: thesis:
defpred S₁[ Nat] means for l being Linear_Combination of B st card (Carrier l) = $1 holds
T . (Sum l) in Lin A;
IA: S₁[ 0 ]

proof

let l be Linear_Combination of B; :: thesis:
assume card (Carrier l) = 0 ; :: thesis:
then Carrier l = {} ;
then l = ZeroLC U by VECTSP_6:def 3;
then Sum l = 0. U by VECTSP_6:15;
then C: T . (Sum l) = 0. V by RANKNULL:9;
0. (Lin A) = 0. V by VECTSP_4:def 2;
hence T . (Sum l) in Lin A by C; :: thesis:

end;

IS: now :: thesis:

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

now :: thesis:

let l be Linear_Combination of B; :: thesis:
assume B1: card (Carrier l) = k + 1 ; :: thesis:
then Carrier l <> {} ;
then consider o being object such that
B2: o in Carrier l by XBOOLE_0:def 1;
consider u being Element of U such that
B3: ( o = u & l . u <> 0. F ) by B2;
defpred S₂[ object , object ] means ( ( $1 = u & $2 = l . 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;
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 VECTSP_6:def 1;

now :: thesis:

let o be object ; :: thesis:
assume o in Carrier l1 ; :: thesis:
then consider v being Element of U such that
C1: ( o = v & l1 . v <> 0. F ) ;
( v = u & l1 . v = l . u ) by B5, C1;
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;
then C1: o in Carrier l by B3;
Carrier l c= B by VECTSP_6:def 4;
hence o in B by C1; :: thesis:

end;

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

proof

now :: thesis:

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

end;

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

end;

reconsider l2 = l - l1 as Linear_Combination of B by VECTSP_6:42;
C1: Carrier l2 = (Carrier l) \ (Carrier l1)

proof

C4: now :: thesis:

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

C6: now :: thesis:

assume C7: v = u ; :: thesis:
l2 . v = (l . v) - (l1 . v) by VECTSP_6:40
.= (l . v) - (l . v) by B5, C7 ;
hence contradiction by C5, RLVECT_1:15; :: thesis:

end;

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

end;

now :: thesis:

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

end;

hence Carrier l2 = (Carrier l) \ (Carrier l1) by C4, TARSKI:2; :: thesis:

end;

now :: thesis:

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

end;

then Carrier l1 c= Carrier l ;
then C2: card ((Carrier l) \ (Carrier l1)) = (card (Carrier l)) - (card (Carrier l1)) by CARD_2:44
.= (k + 1) - 1 by B1, B8, CARD_2:42 ;
C4: T . (Sum l1) = T . ((l1 . u) * u) by B8, VECTSP_6:20
.= (l1 . u) * (T . u) by MOD_2:def 2 ;
C5: Carrier l c= B by VECTSP_6:def 4;
u in the carrier of U ;
then u in dom T by FUNCT_2:def 1;
then T . u in T .: B by C5, B2, B3, FUNCT_1:108;
then T . u in Lin A by AS, VECTSP_7:8;
then consider ll being Linear_Combination of A such that
C6: T . u = Sum ll by VECTSP_7:7;
C7: (l1 . u) * ll is Linear_Combination of A by VECTSP_6:31;
Sum ((l1 . u) * ll) = (l1 . u) * (T . u) by C6, VECTSP_7:22;
then consider l5 being Linear_Combination of A such that
D1: T . (Sum l1) = Sum l5 by C4, C7;
consider l6 being Linear_Combination of A such that
D2: T . (Sum l2) = Sum l6 by IV, C1, C2, VECTSP_7:7;
D3: l5 + l6 is Linear_Combination of A by VECTSP_6:24;
D4: Sum (l5 + l6) = (T . (Sum l1)) + (T . (Sum l2)) by D1, D2, VECTSP_6:44;
Sum l = (Sum l1) + (Sum l2)

proof

reconsider l3 = l as Linear_Combination of U ;
Sum l2 = (Sum l) - (Sum l1) by VECTSP_6:47;
hence (Sum l1) + (Sum l2) = (Sum l) + ((- (Sum l1)) + (Sum l1)) by RLVECT_1:def 3
.= (Sum l3) + (0. U) by RLVECT_1:5
.= Sum l ;
:: thesis:

end;

hence T . (Sum l) in Lin A by D3, D4, VECTSP_7:7, VECTSP_1:def 20; :: 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 l) = n ;
thus T . (Sum l) in Lin A by H, I; :: thesis: