let T be non empty TopSpace; :: thesis: for m being non zero Nat

for f being Function of T,R^1 holds f = (PROJ (m,m)) * (incl (f,m))

let m be non zero Nat; :: thesis: for f being Function of T,R^1 holds f = (PROJ (m,m)) * (incl (f,m))

let f be Function of T,R^1; :: thesis: f = (PROJ (m,m)) * (incl (f,m))

let p be Point of T; :: according to FUNCT_2:def 8 :: thesis: f . p = ((PROJ (m,m)) * (incl (f,m))) . p

set I = incl (f,m);

reconsider G = m |-> (f . p) as FinSequence of REAL ;

1 <= m by NAT_1:14;

then A1: m in Seg m ;

A2: dom (m |-> (f . p)) = Seg m ;

thus ((PROJ (m,m)) * (incl (f,m))) . p = (PROJ (m,m)) . ((incl (f,m)) . p) by FUNCT_2:15

.= ((incl (f,m)) . p) /. m by Def6

.= G /. m by Def4

.= G . m by A1, A2, PARTFUN1:def 6

.= f . p by A1, FINSEQ_2:57 ; :: thesis: verum

for f being Function of T,R^1 holds f = (PROJ (m,m)) * (incl (f,m))

let m be non zero Nat; :: thesis: for f being Function of T,R^1 holds f = (PROJ (m,m)) * (incl (f,m))

let f be Function of T,R^1; :: thesis: f = (PROJ (m,m)) * (incl (f,m))

let p be Point of T; :: according to FUNCT_2:def 8 :: thesis: f . p = ((PROJ (m,m)) * (incl (f,m))) . p

set I = incl (f,m);

reconsider G = m |-> (f . p) as FinSequence of REAL ;

1 <= m by NAT_1:14;

then A1: m in Seg m ;

A2: dom (m |-> (f . p)) = Seg m ;

thus ((PROJ (m,m)) * (incl (f,m))) . p = (PROJ (m,m)) . ((incl (f,m)) . p) by FUNCT_2:15

.= ((incl (f,m)) . p) /. m by Def6

.= G /. m by Def4

.= G . m by A1, A2, PARTFUN1:def 6

.= f . p by A1, FINSEQ_2:57 ; :: thesis: verum