let n be Nat; :: thesis: for T being non empty TopSpace
for f being Function of T,(TOP-REAL n)
for g being Function of T,R^1 holds f <-> g = f <--> (incl g,n)
let T be non empty TopSpace; :: thesis: for f being Function of T,(TOP-REAL n)
for g being Function of T,R^1 holds f <-> g = f <--> (incl g,n)
let f be Function of T,(TOP-REAL n); :: thesis: for g being Function of T,R^1 holds f <-> g = f <--> (incl g,n)
let g be Function of T,R^1 ; :: thesis: f <-> g = f <--> (incl g,n)
set I = incl g,n;
reconsider h = f <-> g as Function of T,(TOP-REAL n) by Th44;
reconsider G = f <--> (incl g,n) as Function of T,(TOP-REAL n) by Th40;
h = G

proof

let t be Point of T; :: according to FUNCT_2:def 9 :: thesis: h . t = G . t
A1: dom h = the carrier of T by FUNCT_2:def 1;
A3: (f . t) - ((incl g,n) . t) = (f . t) - (g . t)

proof

A4: ( dom (f . t) = Seg n & dom ((incl g,n) . t) = Seg n ) by EUCLID:3;
A5: dom ((f . t) - ((incl g,n) . t)) = (dom (f . t)) /\ (dom ((incl g,n) . t)) by VALUED_1:12
.= Seg n by A4 ;
A6: dom ((f . t) - (g . t)) = dom (f . t) by VALUED_1:def 2;
thus dom ((f . t) - ((incl g,n) . t)) = dom ((f . t) - (g . t)) by A5, EUCLID:3; :: according to FUNCT_1:def 17 :: thesis: for b₁ being set holds
( not b₁ in proj1 ((f . t) - ((incl g,n) . t)) or ((f . t) - ((incl g,n) . t)) . b₁ = ((f . t) - (g . t)) . b₁ )
let x be set ; :: thesis: ( not x in proj1 ((f . t) - ((incl g,n) . t)) or ((f . t) - ((incl g,n) . t)) . x = ((f . t) - (g . t)) . x )
assume A7: x in dom ((f . t) - ((incl g,n) . t)) ; :: thesis: ((f . t) - ((incl g,n) . t)) . x = ((f . t) - (g . t)) . x
hence ((f . t) - ((incl g,n) . t)) . x = ((f . t) . x) - (((incl g,n) . t) . x) by VALUED_1:13
.= ((f . t) . x) - (g . t) by A5, A7, Th47
.= ((f . t) - (g . t)) . x by A4, A5, A7, A6, VALUED_1:def 2 ;
:: thesis: verum

end;

dom G = the carrier of T by FUNCT_2:def 1;
hence G . t = (f . t) - ((incl g,n) . t) by VALUED_2:def 46
.= h . t by A1, A3, VALUED_2:62 ;
:: thesis: verum

end;

hence f <-> g = f <--> (incl g,n) ; :: thesis: verum