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 9 :: thesis: f . p = ((PROJ m,m) * (incl f,m)) . p
set I = incl f,m;
reconsider F = (incl f,m) . p as FinSequence of REAL by EUCLID:27;
reconsider G = m |-> (f . p) as FinSequence of REAL ;
A1: m in NAT by ORDINAL1:def 13;
1 <= m by NAT_1:14;
then A2: m in Seg m by A1;
A3: dom (m |-> (f . p)) = Seg m by FUNCOP_1:19;
thus ((PROJ m,m) * (incl f,m)) . p = (PROJ m,m) . ((incl f,m) . p) by FUNCT_2:21
.= ((incl f,m) . p) /. m by Def6
.= G /. m by Def4
.= G . m by A2, A3, PARTFUN1:def 8
.= f . p by A2, FINSEQ_2:71 ; :: thesis: verum