let F be Field; :: thesis:
let U, V be VectSp of F; :: thesis:
let B be Basis of U; :: thesis:
let T1, T2 be linear-transformation of U,V; :: thesis:
assume AS: T1 | B = T2 | B ; :: thesis:
defpred S₁[ Nat] means for l being Linear_Combination of B st card (Carrier l) = $1 holds
T1 . (Sum l) = T2 . (Sum l);
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 A: Sum l = 0. U by VECTSP_6:15;
hence T1 . (Sum l) = 0. V by RANKNULL:9
.= T2 . (Sum l) by A, RANKNULL:9 ;
:: 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} ;

B7: 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;

then B9: Sum l1 = (l1 . u) * u by VECTSP_6:20;
reconsider l2 = l - l1 as Linear_Combination of B by VECTSP_6:42;
C0: T1 . (Sum l1) = T2 . (Sum l1)

proof

D1: u in Carrier l1 by B8, TARSKI:def 1;
then D2: T1 . u = (T2 | B) . u by B7, AS, FUNCT_1:49
.= T2 . u by D1, B7, FUNCT_1:49 ;
thus T1 . (Sum l1) = (l1 . u) * (T1 . u) by B9, MOD_2:def 2
.= T2 . (Sum l1) by D2, B9, MOD_2:def 2 ; :: thesis:

end;

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 card ((Carrier l) \ (Carrier l1)) = (card (Carrier l)) - (card (Carrier l1)) by CARD_2:44
.= (k + 1) - 1 by B1, B8, CARD_2:42 ;
then C2: T1 . (Sum l2) = T2 . (Sum l2) by IV, C1;
C3: 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;

thus T1 . (Sum l) = (T1 . (Sum l1)) + (T1 . (Sum l2)) by C3, VECTSP_1:def 20
.= T2 . (Sum l) by C0, C2, C3, 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);
H: Lin B = ModuleStr(# the carrier of U, the addF of U, the ZeroF of U, the lmult of U #) by VECTSP_7:def 3;

now :: thesis:

let o be object ; :: thesis:
assume o in the carrier of U ; :: thesis:
then o in { (Sum l) where l is Linear_Combination of B : verum } by H, VECTSP_7:def 2;
then consider l being Linear_Combination of B such that
A: o = Sum l ;
consider n being Nat such that
H: card (Carrier l) = n ;
thus T1 . o = T2 . o by A, I, H; :: thesis:

end;

hence T1 = T2 by FUNCT_2:12; :: thesis: