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 ;
A1: m in NAT by ORDINAL1:def 12;
1 <= m by NAT_1:14;
then A2: m in Seg m by A1;
A3: dom (m |-> (f . p)) = Seg m by FUNCOP_1:13;
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 A2, A3, PARTFUN1:def 6
.= f . p by A2, FINSEQ_2:57 ; :: thesis: verum