let n be Nat; :: thesis: for f being additive homogeneous Function of (),()
for A being Subset of () st f | A = id A holds
f | (Lin A) = id (Lin A)

let f be additive homogeneous Function of (),(); :: thesis: for A being Subset of () st f | A = id A holds
f | (Lin A) = id (Lin A)

set TR = TOP-REAL n;
let A be Subset of (); :: 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 S1[ Nat] means for L being Linear_Combination of A st card () <= \$1 holds
f . (Sum L) = Sum L;
A2: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A3: S1[i] ; :: thesis: S1[i + 1]
set i1 = i + 1;
let L be Linear_Combination of A; :: thesis: ( card () <= i + 1 implies f . (Sum L) = Sum L )
assume A4: card () <= i + 1 ; :: thesis: f . (Sum L) = Sum L
per cases ( card () <= i or card () = i + 1 ) by ;
suppose card () <= i ; :: thesis: f . (Sum L) = Sum L
hence f . (Sum L) = Sum L by A3; :: thesis: verum
end;
suppose A5: card () = 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 () by A6;
reconsider X = {x} as Subset of () 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 ;
then ( Carrier K c= {x} & x in Carrier K ) by ;
then A8: Carrier K = {x} by ZFMISC_1:33;
{x} \/ () = Carrier L by ;
then A9: Carrier (L - K) c= Carrier L by ;
(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 ;
then card (Carrier (L - K)) < i + 1 by ;
then A10: card (Carrier (L - K)) <= i by NAT_1:13;
ZeroLC () = (- 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 ;
then A13: f . x = x by ;
Carrier (L - K) c= A by ;
then L - K is Linear_Combination of A by RLVECT_2:def 6;
then A14: f . (Sum (L - K)) = Sum (L - K) by ;
Sum K = (L . x) * x by ;
then f . (Sum K) = Sum K by ;
hence f . (Sum L) = Sum L by ; :: 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 () by RLSUB_1:def 2;
then A15: f | (Lin A) = f | the carrier of (Lin A) by TMAP_1:def 3;
A16: S1[ 0 ]
proof
let L be Linear_Combination of A; :: thesis: ( card () <= 0 implies f . (Sum L) = Sum L )
assume card () <= 0 ; :: thesis: f . (Sum L) = Sum L
then Carrier L = {} ;
then L is Linear_Combination of {} the carrier of () by RLVECT_2:def 6;
then A17: Sum L = 0. () by RLVECT_2:31;
f . (0. ()) = f . (0 * (0. ())) by RLVECT_1:10
.= 0 * (f . (0. ())) by TOPREAL9:def 4
.= 0. () by RLVECT_1:10 ;
hence f . (Sum L) = Sum L by A17; :: thesis: verum
end;
A18: for i being Nat holds S1[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;
S1[ card ()] by A18;
then A22: f . x = x by A21;
(f | (Lin A)) . x = f . x by ;
hence (f | (Lin A)) . x = (id (Lin A)) . x by ; :: 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 ; :: thesis: verum