let n be Nat; :: thesis: for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n)
for A being Subset of (TOP-REAL n) st f | A = id A holds
f | (Lin A) = id (Lin A)
let f be additive homogeneous Function of (TOP-REAL n),(TOP-REAL n); :: thesis: for A being Subset of (TOP-REAL n) st f | A = id A holds
f | (Lin A) = id (Lin A)
set TR = TOP-REAL n;
let A be Subset of (TOP-REAL n); :: thesis: ( f | A = id A implies f | (Lin A) = id (Lin A) )
assume A1: f | A = id A ; :: thesis: f | (Lin A) = id (Lin A)
defpred S₁[ Nat] means for L being Linear_Combination of A st card (Carrier L) <= $1 holds
f . (Sum L) = Sum L;
A2: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A3: S₁[i] ; :: thesis: S₁[i + 1]
set i1 = i + 1;
let L be Linear_Combination of A; :: thesis: ( card (Carrier L) <= i + 1 implies f . (Sum L) = Sum L )
assume A4: card (Carrier L) <= i + 1 ; :: thesis: f . (Sum L) = Sum L

per cases ( card (Carrier L) <= i or card (Carrier L) = i + 1 ) by A4, NAT_1:8;

suppose card (Carrier L) <= i ; :: thesis: f . (Sum L) = Sum L

hence f . (Sum L) = Sum L by A3; :: thesis: verum

end;

suppose A5: card (Carrier L) = i + 1 ; :: thesis: f . (Sum L) = Sum L

then not Carrier L is empty ;
then consider x being object such that
A6: x in Carrier L by XBOOLE_0:def 1;
reconsider x = x as Point of (TOP-REAL n) by A6;
reconsider X = {x} as Subset of (TOP-REAL n) by ZFMISC_1:31;
consider K being Linear_Combination of X such that
A7: K . x = L . x by RLVECT_4:37;
L . x <> 0 by A6, RLVECT_2:19;
then ( Carrier K c= {x} & x in Carrier K ) by A7, RLVECT_2:19, RLVECT_2:def 6;
then A8: Carrier K = {x} by ZFMISC_1:33;
{x} \/ (Carrier L) = Carrier L by A6, ZFMISC_1:40;
then A9: Carrier (L - K) c= Carrier L by A8, RLVECT_2:55;
(L - K) . x = (L . x) - (K . x) by RLVECT_2:54
.= 0 by A7 ;
then not x in Carrier (L - K) by RLVECT_2:19;
then Carrier (L - K) c< Carrier L by A6, A9, XBOOLE_0:def 8;
then card (Carrier (L - K)) < i + 1 by A5, CARD_2:48;
then A10: card (Carrier (L - K)) <= i by NAT_1:13;
ZeroLC (TOP-REAL n) = (- K) - (- K) by RLVECT_2:57
.= (- K) + (- (- K)) by RLVECT_2:def 13
.= (- K) + K by RLVECT_2:53 ;
then L = L + ((- K) + K) by RLVECT_2:41
.= (L + (- K)) + K by RLVECT_2:40
.= (L - K) + K by RLVECT_2:def 13 ;
then A11: Sum L = (Sum (L - K)) + (Sum K) by RLVECT_3:1;
A12: Carrier L c= A by RLVECT_2:def 6;
then (f | A) . x = f . x by A6, FUNCT_1:49;
then A13: f . x = x by A1, A6, A12, FUNCT_1:17;
Carrier (L - K) c= A by A9, A12;
then L - K is Linear_Combination of A by RLVECT_2:def 6;
then A14: f . (Sum (L - K)) = Sum (L - K) by A3, A10;
Sum K = (L . x) * x by A7, RLVECT_2:32;
then f . (Sum K) = Sum K by A13, TOPREAL9:def 4;
hence f . (Sum L) = Sum L by A11, A14, VECTSP_1:def 20; :: thesis: verum

end;

end;

end;

set L = Lin A;
set cL = the carrier of (Lin A);
the carrier of (Lin A) c= the carrier of (TOP-REAL n) by RLSUB_1:def 2;
then A15: f | (Lin A) = f | the carrier of (Lin A) by TMAP_1:def 3;
A16: S₁[ 0 ]

proof

let L be Linear_Combination of A; :: thesis: ( card (Carrier L) <= 0 implies f . (Sum L) = Sum L )
assume card (Carrier L) <= 0 ; :: thesis: f . (Sum L) = Sum L
then Carrier L = {} ;
then L is Linear_Combination of {} the carrier of (TOP-REAL n) by RLVECT_2:def 6;
then A17: Sum L = 0. (TOP-REAL n) by RLVECT_2:31;
f . (0. (TOP-REAL n)) = f . (0 * (0. (TOP-REAL n))) by RLVECT_1:10
.= 0 * (f . (0. (TOP-REAL n))) by TOPREAL9:def 4
.= 0. (TOP-REAL n) by RLVECT_1:10 ;
hence f . (Sum L) = Sum L by A17; :: thesis: verum

end;

A18: for i being Nat holds S₁[i] from NAT_1:sch 2(A16, A2);
A19: for x being object st x in the carrier of (Lin A) holds
(f | (Lin A)) . x = (id (Lin A)) . x

proof

let x be object ; :: thesis: ( x in the carrier of (Lin A) implies (f | (Lin A)) . x = (id (Lin A)) . x )
assume A20: x in the carrier of (Lin A) ; :: thesis: (f | (Lin A)) . x = (id (Lin A)) . x
then x in Lin A ;
then consider K being Linear_Combination of A such that
A21: Sum K = x by RLVECT_3:14;
S₁[ card (Carrier K)] by A18;
then A22: f . x = x by A21;
(f | (Lin A)) . x = f . x by A15, A20, FUNCT_1:49;
hence (f | (Lin A)) . x = (id (Lin A)) . x by A20, A22, FUNCT_1:17; :: thesis: verum

end;

( dom (f | (Lin A)) = the carrier of (Lin A) & dom (id (Lin A)) = the carrier of (Lin A) ) by FUNCT_2:def 1;
hence f | (Lin A) = id (Lin A) by A19, FUNCT_1:2; :: thesis: verum