let n be Nat; :: thesis: for T being non empty TopSpace
for f being Function of T,()
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,()
for g being Function of T,R^1 holds f <#> g = f <##> (incl (g,n))

let f be Function of T,(); :: 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,() by Th45;
reconsider G = f <##> (incl (g,n)) as Function of T,() by Th41;
h = G
proof
let t be Point of T; :: according to FUNCT_2:def 8 :: thesis: 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 4
.= Seg n by A3 ;
hence dom ((f . t) (#) ((incl (g,n)) . t)) = dom ((f . t) (#) (g . t)) by FINSEQ_1:89; :: according to FUNCT_1:def 11 :: thesis: 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 ; :: thesis: ( not x in dom ((f . t) (#) ((incl (g,n)) . t)) or ((f . t) (#) ((incl (g,n)) . t)) . x = ((f . t) (#) (g . t)) . x )
assume A5: 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:def 4
.= ((f . t) . x) * (g . t) by A4, A5, Th47
.= ((f . t) (#) (g . t)) . x by VALUED_1:6 ;
:: 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 47
.= h . t by ;
:: thesis: verum
end;
hence f <#> g = f <##> (incl (g,n)) ; :: thesis: verum