let K be Field; :: thesis: for V1, V2 being finite-dimensional VectSp of K

for f1, f2 being Function of V1,V2 st f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous holds

for b1 being OrdBasis of V1 st len b1 > 0 & f1 * b1 = f2 * b1 holds

f1 = f2

let V1, V2 be finite-dimensional VectSp of K; :: thesis: for f1, f2 being Function of V1,V2 st f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous holds

for b1 being OrdBasis of V1 st len b1 > 0 & f1 * b1 = f2 * b1 holds

f1 = f2

let f1, f2 be Function of V1,V2; :: thesis: ( f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous implies for b1 being OrdBasis of V1 st len b1 > 0 & f1 * b1 = f2 * b1 holds

f1 = f2 )

assume that

A1: ( f1 is additive & f1 is homogeneous ) and

A2: ( f2 is additive & f2 is homogeneous ) ; :: thesis: for b1 being OrdBasis of V1 st len b1 > 0 & f1 * b1 = f2 * b1 holds

f1 = f2

let b1 be OrdBasis of V1; :: thesis: ( len b1 > 0 & f1 * b1 = f2 * b1 implies f1 = f2 )

assume A3: len b1 > 0 ; :: thesis: ( not f1 * b1 = f2 * b1 or f1 = f2 )

reconsider b = rng b1 as Basis of V1 by Def2;

assume A4: f1 * b1 = f2 * b1 ; :: thesis: f1 = f2

for f1, f2 being Function of V1,V2 st f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous holds

for b1 being OrdBasis of V1 st len b1 > 0 & f1 * b1 = f2 * b1 holds

f1 = f2

let V1, V2 be finite-dimensional VectSp of K; :: thesis: for f1, f2 being Function of V1,V2 st f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous holds

for b1 being OrdBasis of V1 st len b1 > 0 & f1 * b1 = f2 * b1 holds

f1 = f2

let f1, f2 be Function of V1,V2; :: thesis: ( f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous implies for b1 being OrdBasis of V1 st len b1 > 0 & f1 * b1 = f2 * b1 holds

f1 = f2 )

assume that

A1: ( f1 is additive & f1 is homogeneous ) and

A2: ( f2 is additive & f2 is homogeneous ) ; :: thesis: for b1 being OrdBasis of V1 st len b1 > 0 & f1 * b1 = f2 * b1 holds

f1 = f2

let b1 be OrdBasis of V1; :: thesis: ( len b1 > 0 & f1 * b1 = f2 * b1 implies f1 = f2 )

assume A3: len b1 > 0 ; :: thesis: ( not f1 * b1 = f2 * b1 or f1 = f2 )

reconsider b = rng b1 as Basis of V1 by Def2;

assume A4: f1 * b1 = f2 * b1 ; :: thesis: f1 = f2

now :: thesis: for v being Element of V1 holds f1 . v = f2 . v

hence
f1 = f2
by FUNCT_2:63; :: thesis: verum
len b1 in Seg (len b1)
by A3, FINSEQ_1:3;

then reconsider D = dom b1 as non empty set by FINSEQ_1:def 3;

let v be Element of V1; :: thesis: f1 . v = f2 . v

Lin b = ModuleStr(# the carrier of V1, the addF of V1, the ZeroF of V1, the lmult of V1 #) by VECTSP_7:def 3;

then v in Lin b by RLVECT_1:1;

then consider KL being Linear_Combination of b such that

A5: v = Sum KL by VECTSP_7:7;

set p = KL (#) b1;

set A = { ((KL . (b1 /. i)) * (b1 /. i)) where i is Element of D : verum } ;

A6: rng (KL (#) b1) c= { ((KL . (b1 /. i)) * (b1 /. i)) where i is Element of D : verum }

f1 . w = f2 . w

hence f1 . v = f1 . (Sum (KL (#) b1)) by A5, Th20

.= f2 . (Sum (KL (#) b1)) by A1, A2, A6, A10, Th21

.= f2 . v by A5, A12, Th20 ;

:: thesis: verum

end;then reconsider D = dom b1 as non empty set by FINSEQ_1:def 3;

let v be Element of V1; :: thesis: f1 . v = f2 . v

Lin b = ModuleStr(# the carrier of V1, the addF of V1, the ZeroF of V1, the lmult of V1 #) by VECTSP_7:def 3;

then v in Lin b by RLVECT_1:1;

then consider KL being Linear_Combination of b such that

A5: v = Sum KL by VECTSP_7:7;

set p = KL (#) b1;

set A = { ((KL . (b1 /. i)) * (b1 /. i)) where i is Element of D : verum } ;

A6: rng (KL (#) b1) c= { ((KL . (b1 /. i)) * (b1 /. i)) where i is Element of D : verum }

proof

A10:
for w being Element of V1 st w in { ((KL . (b1 /. i)) * (b1 /. i)) where i is Element of D : verum } holds
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (KL (#) b1) or x in { ((KL . (b1 /. i)) * (b1 /. i)) where i is Element of D : verum } )

assume x in rng (KL (#) b1) ; :: thesis: x in { ((KL . (b1 /. i)) * (b1 /. i)) where i is Element of D : verum }

then consider i being Nat such that

A7: i in dom (KL (#) b1) and

A8: (KL (#) b1) . i = x by FINSEQ_2:10;

dom (KL (#) b1) = Seg (len (KL (#) b1)) by FINSEQ_1:def 3;

then i in Seg (len b1) by A7, VECTSP_6:def 5;

then A9: i in dom b1 by FINSEQ_1:def 3;

(KL (#) b1) . i = (KL . (b1 /. i)) * (b1 /. i) by A7, VECTSP_6:def 5;

hence x in { ((KL . (b1 /. i)) * (b1 /. i)) where i is Element of D : verum } by A8, A9; :: thesis: verum

end;assume x in rng (KL (#) b1) ; :: thesis: x in { ((KL . (b1 /. i)) * (b1 /. i)) where i is Element of D : verum }

then consider i being Nat such that

A7: i in dom (KL (#) b1) and

A8: (KL (#) b1) . i = x by FINSEQ_2:10;

dom (KL (#) b1) = Seg (len (KL (#) b1)) by FINSEQ_1:def 3;

then i in Seg (len b1) by A7, VECTSP_6:def 5;

then A9: i in dom b1 by FINSEQ_1:def 3;

(KL (#) b1) . i = (KL . (b1 /. i)) * (b1 /. i) by A7, VECTSP_6:def 5;

hence x in { ((KL . (b1 /. i)) * (b1 /. i)) where i is Element of D : verum } by A8, A9; :: thesis: verum

f1 . w = f2 . w

proof

A12:
( b1 is one-to-one & Carrier KL c= rng b1 )
by Def2, VECTSP_6:def 4;
let w be Element of V1; :: thesis: ( w in { ((KL . (b1 /. i)) * (b1 /. i)) where i is Element of D : verum } implies f1 . w = f2 . w )

assume w in { ((KL . (b1 /. i)) * (b1 /. i)) where i is Element of D : verum } ; :: thesis: f1 . w = f2 . w

then consider i being Element of D such that

A11: w = (KL . (b1 /. i)) * (b1 /. i) ;

f1 . (b1 /. i) = f1 . (b1 . i) by PARTFUN1:def 6

.= (f2 * b1) . i by A4, FUNCT_1:13

.= f2 . (b1 . i) by FUNCT_1:13

.= f2 . (b1 /. i) by PARTFUN1:def 6 ;

then f1 . ((KL . (b1 /. i)) * (b1 /. i)) = (KL . (b1 /. i)) * (f2 . (b1 /. i)) by A1, MOD_2:def 2

.= f2 . ((KL . (b1 /. i)) * (b1 /. i)) by A2, MOD_2:def 2 ;

hence f1 . w = f2 . w by A11; :: thesis: verum

end;assume w in { ((KL . (b1 /. i)) * (b1 /. i)) where i is Element of D : verum } ; :: thesis: f1 . w = f2 . w

then consider i being Element of D such that

A11: w = (KL . (b1 /. i)) * (b1 /. i) ;

f1 . (b1 /. i) = f1 . (b1 . i) by PARTFUN1:def 6

.= (f2 * b1) . i by A4, FUNCT_1:13

.= f2 . (b1 . i) by FUNCT_1:13

.= f2 . (b1 /. i) by PARTFUN1:def 6 ;

then f1 . ((KL . (b1 /. i)) * (b1 /. i)) = (KL . (b1 /. i)) * (f2 . (b1 /. i)) by A1, MOD_2:def 2

.= f2 . ((KL . (b1 /. i)) * (b1 /. i)) by A2, MOD_2:def 2 ;

hence f1 . w = f2 . w by A11; :: thesis: verum

hence f1 . v = f1 . (Sum (KL (#) b1)) by A5, Th20

.= f2 . (Sum (KL (#) b1)) by A1, A2, A6, A10, Th21

.= f2 . v by A5, A12, Th20 ;

:: thesis: verum