let n be non zero Element of NAT ; :: thesis: for h being PartFunc of REAL,(REAL n) holds

( h is continuous iff for i being Element of NAT st i in Seg n holds

(proj (i,n)) * h is continuous )

let h be PartFunc of REAL,(REAL n); :: thesis: ( h is continuous iff for i being Element of NAT st i in Seg n holds

(proj (i,n)) * h is continuous )

(proj (i,n)) * h is continuous ; :: thesis: h is continuous

let x0 be Real; :: according to NFCONT_4:def 5 :: thesis: ( x0 in dom h implies h is_continuous_in x0 )

assume A6: x0 in dom h ; :: thesis: h is_continuous_in x0

( h is continuous iff for i being Element of NAT st i in Seg n holds

(proj (i,n)) * h is continuous )

let h be PartFunc of REAL,(REAL n); :: thesis: ( h is continuous iff for i being Element of NAT st i in Seg n holds

(proj (i,n)) * h is continuous )

hereby :: thesis: ( ( for i being Element of NAT st i in Seg n holds

(proj (i,n)) * h is continuous ) implies h is continuous )

assume A5:
for i being Element of NAT st i in Seg n holds (proj (i,n)) * h is continuous ) implies h is continuous )

assume A1:
h is continuous
; :: thesis: for i being Element of NAT st i in Seg n holds

(proj (i,n)) * h is continuous

thus for i being Element of NAT st i in Seg n holds

(proj (i,n)) * h is continuous :: thesis: verum

end;(proj (i,n)) * h is continuous

thus for i being Element of NAT st i in Seg n holds

(proj (i,n)) * h is continuous :: thesis: verum

proof

let i be Element of NAT ; :: thesis: ( i in Seg n implies (proj (i,n)) * h is continuous )

assume A2: i in Seg n ; :: thesis: (proj (i,n)) * h is continuous

A3: dom (proj (i,n)) = REAL n by FUNCT_2:def 1;

rng h c= REAL n ;

then A4: dom ((proj (i,n)) * h) = dom h by A3, RELAT_1:27;

end;assume A2: i in Seg n ; :: thesis: (proj (i,n)) * h is continuous

A3: dom (proj (i,n)) = REAL n by FUNCT_2:def 1;

rng h c= REAL n ;

then A4: dom ((proj (i,n)) * h) = dom h by A3, RELAT_1:27;

now :: thesis: for x0 being Real st x0 in dom ((proj (i,n)) * h) holds

(proj (i,n)) * h is_continuous_in x0

hence
(proj (i,n)) * h is continuous
; :: thesis: verum(proj (i,n)) * h is_continuous_in x0

let x0 be Real; :: thesis: ( x0 in dom ((proj (i,n)) * h) implies (proj (i,n)) * h is_continuous_in x0 )

assume x0 in dom ((proj (i,n)) * h) ; :: thesis: (proj (i,n)) * h is_continuous_in x0

then h is_continuous_in x0 by A1, A4;

hence (proj (i,n)) * h is_continuous_in x0 by A2, Th43; :: thesis: verum

end;assume x0 in dom ((proj (i,n)) * h) ; :: thesis: (proj (i,n)) * h is_continuous_in x0

then h is_continuous_in x0 by A1, A4;

hence (proj (i,n)) * h is_continuous_in x0 by A2, Th43; :: thesis: verum

(proj (i,n)) * h is continuous ; :: thesis: h is continuous

let x0 be Real; :: according to NFCONT_4:def 5 :: thesis: ( x0 in dom h implies h is_continuous_in x0 )

assume A6: x0 in dom h ; :: thesis: h is_continuous_in x0

now :: thesis: for i being Element of NAT st i in Seg n holds

(proj (i,n)) * h is_continuous_in x0

hence
h is_continuous_in x0
by A6, Th43; :: thesis: verum(proj (i,n)) * h is_continuous_in x0

let i be Element of NAT ; :: thesis: ( i in Seg n implies (proj (i,n)) * h is_continuous_in x0 )

assume A7: i in Seg n ; :: thesis: (proj (i,n)) * h is_continuous_in x0

A8: dom (proj (i,n)) = REAL n by FUNCT_2:def 1;

rng h c= REAL n ;

then A9: dom ((proj (i,n)) * h) = dom h by A8, RELAT_1:27;

(proj (i,n)) * h is continuous by A5, A7;

hence (proj (i,n)) * h is_continuous_in x0 by A6, A9; :: thesis: verum

end;assume A7: i in Seg n ; :: thesis: (proj (i,n)) * h is_continuous_in x0

A8: dom (proj (i,n)) = REAL n by FUNCT_2:def 1;

rng h c= REAL n ;

then A9: dom ((proj (i,n)) * h) = dom h by A8, RELAT_1:27;

(proj (i,n)) * h is continuous by A5, A7;

hence (proj (i,n)) * h is_continuous_in x0 by A6, A9; :: thesis: verum