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

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