let x be object ; :: thesis: for n being Nat
for T being non empty TopSpace
for R being real-membered set
for f being Function of T,R
for t being Point of T st x in Seg n holds
((incl (f,n)) . t) . x = f . t
let n be Nat; :: thesis: for T being non empty TopSpace
for R being real-membered set
for f being Function of T,R
for t being Point of T st x in Seg n holds
((incl (f,n)) . t) . x = f . t
let T be non empty TopSpace; :: thesis: for R being real-membered set
for f being Function of T,R
for t being Point of T st x in Seg n holds
((incl (f,n)) . t) . x = f . t
let R be real-membered set ; :: thesis: for f being Function of T,R
for t being Point of T st x in Seg n holds
((incl (f,n)) . t) . x = f . t
let f be Function of T,R; :: thesis: for t being Point of T st x in Seg n holds
((incl (f,n)) . t) . x = f . t
let t be Point of T; :: thesis: ( x in Seg n implies ((incl (f,n)) . t) . x = f . t )
assume A1: x in Seg n ; :: thesis: ((incl (f,n)) . t) . x = f . t
thus ((incl (f,n)) . t) . x = (n |-> (f . t)) . x by Def4
.= f . t by A1, FINSEQ_2:57 ; :: thesis: verum