let A, B be Subset of REAL; for f being Function of [:R^1,R^1:],(TOP-REAL 2) st ( for x, y being Real holds f . [x,y] = <*x,y*> ) holds
f .: [:A,B:] = product ((1,2) --> (A,B))
let f be Function of [:R^1,R^1:],(TOP-REAL 2); ( ( for x, y being Real holds f . [x,y] = <*x,y*> ) implies f .: [:A,B:] = product ((1,2) --> (A,B)) )
assume A1:
for x, y being Real holds f . [x,y] = <*x,y*>
; f .: [:A,B:] = product ((1,2) --> (A,B))
set h = (1,2) --> (A,B);
A2:
dom ((1,2) --> (A,B)) = {1,2}
by FUNCT_4:62;
thus
f .: [:A,B:] c= product ((1,2) --> (A,B))
XBOOLE_0:def 10 product ((1,2) --> (A,B)) c= f .: [:A,B:]proof
let x be
object ;
TARSKI:def 3 ( not x in f .: [:A,B:] or x in product ((1,2) --> (A,B)) )
assume
x in f .: [:A,B:]
;
x in product ((1,2) --> (A,B))
then consider a being
object such that A3:
a in the
carrier of
[:R^1,R^1:]
and A4:
a in [:A,B:]
and A5:
f . a = x
by FUNCT_2:64;
reconsider a =
a as
Point of
[:R^1,R^1:] by A3;
consider m,
n being
object such that A6:
m in A
and A7:
n in B
and A8:
a = [m,n]
by A4, ZFMISC_1:def 2;
f . a = x
by A5;
then reconsider g =
x as
Function of
(Seg 2),
REAL by EUCLID:23;
reconsider m =
m,
n =
n as
Real by A6, A7;
A9:
for
y being
object st
y in dom ((1,2) --> (A,B)) holds
g . y in ((1,2) --> (A,B)) . y
proof
let y be
object ;
( y in dom ((1,2) --> (A,B)) implies g . y in ((1,2) --> (A,B)) . y )
A10:
|[m,n]| `1 = m
by EUCLID:52;
assume
y in dom ((1,2) --> (A,B))
;
g . y in ((1,2) --> (A,B)) . y
then A11:
(
y = 1 or
y = 2 )
by TARSKI:def 2;
A12:
|[m,n]| `2 = n
by EUCLID:52;
f . [m,n] = |[m,n]|
by A1;
hence
g . y in ((1,2) --> (A,B)) . y
by A5, A6, A7, A8, A11, A10, A12, FUNCT_4:63;
verum
end;
dom g = dom ((1,2) --> (A,B))
by A2, FINSEQ_1:2, FUNCT_2:def 1;
hence
x in product ((1,2) --> (A,B))
by A9, CARD_3:9;
verum
end;
A13:
((1,2) --> (A,B)) . 2 = B
by FUNCT_4:63;
let a be object ; TARSKI:def 3 ( not a in product ((1,2) --> (A,B)) or a in f .: [:A,B:] )
assume
a in product ((1,2) --> (A,B))
; a in f .: [:A,B:]
then consider g being Function such that
A14:
a = g
and
A15:
dom g = dom ((1,2) --> (A,B))
and
A16:
for x being object st x in dom ((1,2) --> (A,B)) holds
g . x in ((1,2) --> (A,B)) . x
by CARD_3:def 5;
2 in dom ((1,2) --> (A,B))
by A2, TARSKI:def 2;
then A17:
g . 2 in B
by A13, A16;
A18:
((1,2) --> (A,B)) . 1 = A
by FUNCT_4:63;
1 in dom ((1,2) --> (A,B))
by A2, TARSKI:def 2;
then A19:
g . 1 in A
by A18, A16;
then A20:
f . [(g . 1),(g . 2)] = <*(g . 1),(g . 2)*>
by A1, A17;
A22:
dom <*(g . 1),(g . 2)*> = {1,2}
by FINSEQ_1:2, FINSEQ_1:89;
A23:
[(g . 1),(g . 2)] in [:A,B:]
by A19, A17, ZFMISC_1:87;
the carrier of [:R^1,R^1:] = [: the carrier of R^1, the carrier of R^1:]
by BORSUK_1:def 2;
then
[(g . 1),(g . 2)] in the carrier of [:R^1,R^1:]
by A19, A17, TOPMETR:17, ZFMISC_1:87;
hence
a in f .: [:A,B:]
by A2, A14, A15, A23, A22, A21, A20, FUNCT_1:2, FUNCT_2:35; verum