let X, E, G, F be RealNormSpace; :: thesis: for BL being BilinearOperator of E,F,G
for f being PartFunc of X,E
for g being PartFunc of X,F
for S being Subset of X st BL is_continuous_on the carrier of [:E,F:] & S c= dom f & S c= dom g & ( for s being Point of X st s in S holds
f is_continuous_in s ) & ( for s being Point of X st s in S holds
g is_continuous_in s ) holds
ex H being PartFunc of X,G st
( dom H = S & ( for s being Point of X st s in S holds
H . s = BL . ((f . s),(g . s)) ) & H is_continuous_on S )
let BL be BilinearOperator of E,F,G; :: thesis: for f being PartFunc of X,E
for g being PartFunc of X,F
for S being Subset of X st BL is_continuous_on the carrier of [:E,F:] & S c= dom f & S c= dom g & ( for s being Point of X st s in S holds
f is_continuous_in s ) & ( for s being Point of X st s in S holds
g is_continuous_in s ) holds
ex H being PartFunc of X,G st
( dom H = S & ( for s being Point of X st s in S holds
H . s = BL . ((f . s),(g . s)) ) & H is_continuous_on S )
let f be PartFunc of X,E; :: thesis: for g being PartFunc of X,F
for S being Subset of X st BL is_continuous_on the carrier of [:E,F:] & S c= dom f & S c= dom g & ( for s being Point of X st s in S holds
f is_continuous_in s ) & ( for s being Point of X st s in S holds
g is_continuous_in s ) holds
ex H being PartFunc of X,G st
( dom H = S & ( for s being Point of X st s in S holds
H . s = BL . ((f . s),(g . s)) ) & H is_continuous_on S )
let g be PartFunc of X,F; :: thesis: for S being Subset of X st BL is_continuous_on the carrier of [:E,F:] & S c= dom f & S c= dom g & ( for s being Point of X st s in S holds
f is_continuous_in s ) & ( for s being Point of X st s in S holds
g is_continuous_in s ) holds
ex H being PartFunc of X,G st
( dom H = S & ( for s being Point of X st s in S holds
H . s = BL . ((f . s),(g . s)) ) & H is_continuous_on S )
let S be Subset of X; :: thesis: ( BL is_continuous_on the carrier of [:E,F:] & S c= dom f & S c= dom g & ( for s being Point of X st s in S holds
f is_continuous_in s ) & ( for s being Point of X st s in S holds
g is_continuous_in s ) implies ex H being PartFunc of X,G st
( dom H = S & ( for s being Point of X st s in S holds
H . s = BL . ((f . s),(g . s)) ) & H is_continuous_on S ) )
assume that
A1: BL is_continuous_on the carrier of [:E,F:] and
A2: ( S c= dom f & S c= dom g ) and
A3: for s being Point of X st s in S holds
f is_continuous_in s and
A4: for s being Point of X st s in S holds
g is_continuous_in s ; :: thesis: ex H being PartFunc of X,G st
( dom H = S & ( for s being Point of X st s in S holds
H . s = BL . ((f . s),(g . s)) ) & H is_continuous_on S )
defpred S1[ object , object ] means ex t being Point of X st
( t = $1 & $2 = BL . ((f . t),(g . t)) );
A5: for x being object st x in S holds
ex y being object st
( y in the carrier of G & S1[x,y] )
proof
let x be object ; :: thesis: ( x in S implies ex y being object st
( y in the carrier of G & S1[x,y] ) )
assume A6: x in S ; :: thesis: ex y being object st
( y in the carrier of G & S1[x,y] )
then reconsider t = x as Point of X ;
take y = BL . ((f . t),(g . t)); :: thesis: ( y in the carrier of G & S1[x,y] )
A7: ( f . t in rng f & g . t in rng g ) by A2, A6, FUNCT_1:3;
then reconsider p = f . t as Point of E ;
reconsider q = g . t as Point of F by A7;
[p,q] is Point of [:E,F:] ;
hence ( y in the carrier of G & S1[x,y] ) by FUNCT_2:5; :: thesis: verum
end;
consider H being Function of S,G such that
A8: for z being object st z in S holds
S1[z,H . z] from FUNCT_2:sch 1(A5);
 A9: dom H = S by FUNCT_2:def 1;
rng H c= the carrier of G ;
then H in PFuncs ( the carrier of X, the carrier of G) by A9, PARTFUN1:def 3;
then reconsider H = H as PartFunc of X,G by PARTFUN1:46;
take H ; :: thesis: ( dom H = S & ( for s being Point of X st s in S holds
H . s = BL . ((f . s),(g . s)) ) & H is_continuous_on S )
thus A12: dom H = S by FUNCT_2:def 1; :: thesis: ( ( for s being Point of X st s in S holds
H . s = BL . ((f . s),(g . s)) ) & H is_continuous_on S )
thus A13: for s being Point of X st s in S holds
H . s = BL . ((f . s),(g . s)) :: thesis: H is_continuous_on S
proof
let s be Point of X; :: thesis: ( s in S implies H . s = BL . ((f . s),(g . s)) )
assume s in S ; :: thesis: H . s = BL . ((f . s),(g . s))
then ex t being Point of X st
( t = s & H . s = BL . ((f . t),(g . t)) ) by A8;
hence H . s = BL . ((f . s),(g . s)) ; :: thesis: verum
end;
for x0 being Point of X
for r being Real st x0 in S & 0 < r holds
ex pq being Real st
( 0 < pq & ( for x1 being Point of X st x1 in S & ||.(x1 - x0).|| < pq holds
||.((H /. x1) - (H /. x0)).|| < r ) )
proof
let x0 be Point of X; :: thesis: for r being Real st x0 in S & 0 < r holds
ex pq being Real st
( 0 < pq & ( for x1 being Point of X st x1 in S & ||.(x1 - x0).|| < pq holds
||.((H /. x1) - (H /. x0)).|| < r ) )
let r be Real; :: thesis: ( x0 in S & 0 < r implies ex pq being Real st
( 0 < pq & ( for x1 being Point of X st x1 in S & ||.(x1 - x0).|| < pq holds
||.((H /. x1) - (H /. x0)).|| < r ) ) )
assume A16: ( x0 in S & 0 < r ) ; :: thesis: ex pq being Real st
( 0 < pq & ( for x1 being Point of X st x1 in S & ||.(x1 - x0).|| < pq holds
||.((H /. x1) - (H /. x0)).|| < r ) )
then A17: f is_continuous_in x0 by A3;
A18: g is_continuous_in x0 by A4, A16;
A20: ( f . x0 in rng f & g . x0 in rng g ) by A2, A16, FUNCT_1:3;
[(f . x0),(g . x0)] is set by TARSKI:1;
then reconsider z0 = [(f . x0),(g . x0)] as Point of [:E,F:] by A20, PRVECT_3:18;
consider s being Real such that
A21: ( 0 < s & ( for z1 being Point of [:E,F:] st z1 in the carrier of [:E,F:] & ||.(z1 - z0).|| < s holds
||.((BL /. z1) - (BL /. z0)).|| < r ) ) by A1, A16, NFCONT_1:19;
set s1 = s / 2;
consider p being Real such that
A23: ( 0 < p & ( for x1 being Point of X st x1 in dom f & ||.(x1 - x0).|| < p holds
||.((f /. x1) - (f /. x0)).|| < s / 2 ) ) by A17, A21, NFCONT_1:7, XREAL_1:215;
consider q being Real such that
A24: ( 0 < q & ( for x1 being Point of X st x1 in dom g & ||.(x1 - x0).|| < q holds
||.((g /. x1) - (g /. x0)).|| < s / 2 ) ) by A18, A21, NFCONT_1:7, XREAL_1:215;
set pq = min (p,q);
A25: ( 0 < min (p,q) & min (p,q) <= p & min (p,q) <= q ) by A23, A24, XXREAL_0:15, XXREAL_0:17;
take min (p,q) ; :: thesis: ( 0 < min (p,q) & ( for x1 being Point of X st x1 in S & ||.(x1 - x0).|| < min (p,q) holds
||.((H /. x1) - (H /. x0)).|| < r ) )
thus 0 < min (p,q) by A23, A24, XXREAL_0:15; :: thesis: for x1 being Point of X st x1 in S & ||.(x1 - x0).|| < min (p,q) holds
||.((H /. x1) - (H /. x0)).|| < r
thus for x1 being Point of X st x1 in S & ||.(x1 - x0).|| < min (p,q) holds
||.((H /. x1) - (H /. x0)).|| < r :: thesis: verum
proof
let x1 be Point of X; :: thesis: ( x1 in S & ||.(x1 - x0).|| < min (p,q) implies ||.((H /. x1) - (H /. x0)).|| < r )
assume A26: ( x1 in S & ||.(x1 - x0).|| < min (p,q) ) ; :: thesis: ||.((H /. x1) - (H /. x0)).|| < r
then A27: ( ||.(x1 - x0).|| < p & ||.(x1 - x0).|| < q ) by A25, XXREAL_0:2;
then A29: ||.((f /. x1) - (f /. x0)).|| < s / 2 by A2, A23, A26;
A30: ||.((g /. x1) - (g /. x0)).|| < s / 2 by A2, A24, A26, A27;
A32: ( f . x1 in rng f & g . x1 in rng g ) by A2, A26, FUNCT_1:3;
[(f . x1),(g . x1)] is set by TARSKI:1;
then reconsider z1 = [(f . x1),(g . x1)] as Point of [:E,F:] by A32, PRVECT_3:18;
A33: z1 = [(f /. x1),(g . x1)] by A2, A26, PARTFUN1:def 6
.= [(f /. x1),(g /. x1)] by A2, A26, PARTFUN1:def 6 ;
z0 = [(f /. x0),(g . x0)] by A2, A16, PARTFUN1:def 6
.= [(f /. x0),(g /. x0)] by A2, A16, PARTFUN1:def 6 ;
then - z0 = [(- (f /. x0)),(- (g /. x0))] by PRVECT_3:18;
then z1 - z0 = [((f /. x1) - (f /. x0)),((g /. x1) - (g /. x0))] by A33, PRVECT_3:18;
then A35: ||.(z1 - z0).|| = sqrt ((||.((f /. x1) - (f /. x0)).|| ^2) + (||.((g /. x1) - (g /. x0)).|| ^2)) by NDIFF_8:1;
A36: ||.((f /. x1) - (f /. x0)).|| ^2 <= (s / 2) ^2 by A29, SQUARE_1:15;
||.((g /. x1) - (g /. x0)).|| ^2 <= (s / 2) ^2 by A30, SQUARE_1:15;
then A38: (||.((f /. x1) - (f /. x0)).|| ^2) + (||.((g /. x1) - (g /. x0)).|| ^2) <= ((s ^2) / 4) + ((s ^2) / 4) by A36, XREAL_1:7;
(s ^2) / 2 < s ^2 by A21, XREAL_1:129, XREAL_1:216;
then (||.((f /. x1) - (f /. x0)).|| ^2) + (||.((g /. x1) - (g /. x0)).|| ^2) < s ^2 by A38, XXREAL_0:2;
then sqrt ((||.((f /. x1) - (f /. x0)).|| ^2) + (||.((g /. x1) - (g /. x0)).|| ^2)) < sqrt (s ^2) by SQUARE_1:27;
then A40: ||.(z1 - z0).|| < s by A21, A35, SQUARE_1:22;
A41: H /. x1 = H . x1 by A12, A26, PARTFUN1:def 6
.= BL . ((f . x1),(g . x1)) by A13, A26
.= BL /. z1 ;
H /. x0 = H . x0 by A12, A16, PARTFUN1:def 6
.= BL . ((f . x0),(g . x0)) by A13, A16
.= BL /. z0 ;
hence ||.((H /. x1) - (H /. x0)).|| < r by A21, A40, A41; :: thesis: verum
end;
end;
hence H is_continuous_on S by A12, NFCONT_1:19; :: thesis: verum