let n be Nat; 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; 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); for g being Function of T,R^1 holds f <+> g = f <++> (incl (g,n))
let g be Function of T,R^1; f <+> g = f <++> (incl (g,n))
set I = incl (g,n);
reconsider h = f <+> g as Function of T,(TOP-REAL n) by Th43;
reconsider G = f <++> (incl (g,n)) as Function of T,(TOP-REAL n) by Th39;
h = G
proof
let t be
Point of
T;
FUNCT_2:def 8 h . t = G . t
A1:
dom h = the
carrier of
T
by FUNCT_2:def 1;
A2:
(f . t) + ((incl (g,n)) . t) = (f . t) + (g . t)
proof
A3:
(
dom (f . t) = Seg n &
dom ((incl (g,n)) . t) = Seg n )
by FINSEQ_1:89;
A4:
dom ((f . t) + ((incl (g,n)) . t)) =
(dom (f . t)) /\ (dom ((incl (g,n)) . t))
by VALUED_1:def 1
.=
Seg n
by A3
;
A5:
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 A4, FINSEQ_1:89;
FUNCT_1:def 11 for b1 being object holds
( not b1 in dom ((f . t) + ((incl (g,n)) . t)) or ((f . t) + ((incl (g,n)) . t)) . b1 = ((f . t) + (g . t)) . b1 )
let x be
object ;
( not x in dom ((f . t) + ((incl (g,n)) . t)) or ((f . t) + ((incl (g,n)) . t)) . x = ((f . t) + (g . t)) . x )
assume A6:
x in dom ((f . t) + ((incl (g,n)) . t))
;
((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:def 1
.=
((f . t) . x) + (g . t)
by A4, A6, Th47
.=
((f . t) + (g . t)) . x
by A3, A4, A6, A5, VALUED_1:def 2
;
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 45
.=
h . t
by A1, A2, VALUED_2:def 41
;
verum
end;
hence
f <+> g = f <++> (incl (g,n))
; verum