let S, E, F, G be RealNormSpace; :: thesis: for Z being Subset of S
for u being PartFunc of S,E
for v being PartFunc of S,F
for w being PartFunc of S,[:E,F:] st w = <:u,v:> & u is_continuous_on Z & v is_continuous_on Z holds
w is_continuous_on Z
let Z be Subset of S; :: thesis: for u being PartFunc of S,E
for v being PartFunc of S,F
for w being PartFunc of S,[:E,F:] st w = <:u,v:> & u is_continuous_on Z & v is_continuous_on Z holds
w is_continuous_on Z
let u be PartFunc of S,E; :: thesis: for v being PartFunc of S,F
for w being PartFunc of S,[:E,F:] st w = <:u,v:> & u is_continuous_on Z & v is_continuous_on Z holds
w is_continuous_on Z
let v be PartFunc of S,F; :: thesis: for w being PartFunc of S,[:E,F:] st w = <:u,v:> & u is_continuous_on Z & v is_continuous_on Z holds
w is_continuous_on Z
let w be PartFunc of S,[:E,F:]; :: thesis: ( w = <:u,v:> & u is_continuous_on Z & v is_continuous_on Z implies w is_continuous_on Z )
assume A1: ( w = <:u,v:> & u is_continuous_on Z & v is_continuous_on Z ) ; :: thesis: w is_continuous_on Z
A2: ( Z c= dom u & Z c= dom v ) by A1, NFCONT_1:19;
A3: dom w = (dom u) /\ (dom v) by A1, FUNCT_3:def 7;
then A4: Z c= dom w by A2, XBOOLE_1:19;
for x0 being Point of S
for r being Real st x0 in Z & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of S st x1 in Z & ||.(x1 - x0).|| < s holds
||.((w /. x1) - (w /. x0)).|| < r ) )

proof

let x0 be Point of S; :: thesis: for r being Real st x0 in Z & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of S st x1 in Z & ||.(x1 - x0).|| < s holds
||.((w /. x1) - (w /. x0)).|| < r ) )
let r0 be Real; :: thesis: ( x0 in Z & 0 < r0 implies ex s being Real st
( 0 < s & ( for x1 being Point of S st x1 in Z & ||.(x1 - x0).|| < s holds
||.((w /. x1) - (w /. x0)).|| < r0 ) ) )
assume A5: ( x0 in Z & 0 < r0 ) ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Point of S st x1 in Z & ||.(x1 - x0).|| < s holds
||.((w /. x1) - (w /. x0)).|| < r0 ) )
set rr0 = r0 / 2;
A6: ( 0 < r0 / 2 & r0 / 2 < r0 ) by A5, XREAL_1:215, XREAL_1:216;
set r = (r0 / 2) / 2;
consider s1 being Real such that
A7: ( 0 < s1 & ( for x1 being Point of S st x1 in Z & ||.(x1 - x0).|| < s1 holds
||.((u /. x1) - (u /. x0)).|| < (r0 / 2) / 2 ) ) by A1, A5, A6, NFCONT_1:19, XREAL_1:215;
consider s2 being Real such that
A8: ( 0 < s2 & ( for x1 being Point of S st x1 in Z & ||.(x1 - x0).|| < s2 holds
||.((v /. x1) - (v /. x0)).|| < (r0 / 2) / 2 ) ) by A1, A5, A6, NFCONT_1:19, XREAL_1:215;
reconsider s = min (s1,s2) as Real ;
take s ; :: thesis: ( 0 < s & ( for x1 being Point of S st x1 in Z & ||.(x1 - x0).|| < s holds
||.((w /. x1) - (w /. x0)).|| < r0 ) )
thus 0 < s by A7, A8, XXREAL_0:15; :: thesis: for x1 being Point of S st x1 in Z & ||.(x1 - x0).|| < s holds
||.((w /. x1) - (w /. x0)).|| < r0
let x1 be Point of S; :: thesis: ( x1 in Z & ||.(x1 - x0).|| < s implies ||.((w /. x1) - (w /. x0)).|| < r0 )
assume A9: ( x1 in Z & ||.(x1 - x0).|| < s ) ; :: thesis: ||.((w /. x1) - (w /. x0)).|| < r0
s <= s1 by XXREAL_0:17;
then ||.(x1 - x0).|| < s1 by A9, XXREAL_0:2;
then A10: ||.((u /. x1) - (u /. x0)).|| < (r0 / 2) / 2 by A7, A9;
s <= s2 by XXREAL_0:17;
then ||.(x1 - x0).|| < s2 by A9, XXREAL_0:2;
then A11: ||.((v /. x1) - (v /. x0)).|| < (r0 / 2) / 2 by A8, A9;
A12: w /. x1 = w . x1 by A4, A9, PARTFUN1:def 6
.= [(u . x1),(v . x1)] by A1, A4, A9, FUNCT_3:def 7
.= [(u /. x1),(v . x1)] by A2, A9, PARTFUN1:def 6
.= [(u /. x1),(v /. x1)] by A2, A9, PARTFUN1:def 6 ;
w /. x0 = w . x0 by A4, A5, PARTFUN1:def 6
.= [(u . x0),(v . x0)] by A1, A4, A5, FUNCT_3:def 7
.= [(u /. x0),(v . x0)] by A2, A5, PARTFUN1:def 6
.= [(u /. x0),(v /. x0)] by A2, A5, PARTFUN1:def 6 ;
then - (w /. x0) = [(- (u /. x0)),(- (v /. x0))] by PRVECT_3:18;
then (w /. x1) - (w /. x0) = [((u /. x1) - (u /. x0)),((v /. x1) - (v /. x0))] by A12, PRVECT_3:18;
then A13: ||.((w /. x1) - (w /. x0)).|| <= ||.((u /. x1) - (u /. x0)).|| + ||.((v /. x1) - (v /. x0)).|| by Th17;
||.((u /. x1) - (u /. x0)).|| + ||.((v /. x1) - (v /. x0)).|| <= ((r0 / 2) / 2) + ((r0 / 2) / 2) by A10, A11, XREAL_1:7;
then ||.((w /. x1) - (w /. x0)).|| <= r0 / 2 by A13, XXREAL_0:2;
hence ||.((w /. x1) - (w /. x0)).|| < r0 by A6, XXREAL_0:2; :: thesis: verum

end;

hence w is_continuous_on Z by A2, A3, NFCONT_1:19, XBOOLE_1:19; :: thesis: verum