set f = proj (1,1);
for x1, x2 being object st x1 in dom (proj (1,1)) & x2 in dom (proj (1,1)) & (proj (1,1)) . x1 = (proj (1,1)) . x2 holds
x1 = x2
proof
let x1,
x2 be
object ;
( x1 in dom (proj (1,1)) & x2 in dom (proj (1,1)) & (proj (1,1)) . x1 = (proj (1,1)) . x2 implies x1 = x2 )
assume that A1:
x1 in dom (proj (1,1))
and A2:
x2 in dom (proj (1,1))
and A3:
(proj (1,1)) . x1 = (proj (1,1)) . x2
;
x1 = x2
reconsider y1 =
x1,
y2 =
x2 as
Element of
REAL 1
by A1, A2;
x1 is
Tuple of 1,
REAL
by A1, FINSEQ_2:131;
then consider d1 being
Element of
REAL such that A4:
x1 = <*d1*>
by FINSEQ_2:97;
d1 = <*d1*> . 1
by FINSEQ_1:40;
then
d1 = (proj (1,1)) . y1
by A4, Def1;
then A5:
d1 = y2 . 1
by A3, Def1;
x2 is
Tuple of 1,
REAL
by A2, FINSEQ_2:131;
then
ex
d2 being
Element of
REAL st
x2 = <*d2*>
by FINSEQ_2:97;
hence
x1 = x2
by A4, A5, FINSEQ_1:40;
verum
end;
then A6:
proj (1,1) is one-to-one
by FUNCT_1:def 4;
A7:
dom (proj (1,1)) = REAL 1
by FUNCT_2:def 1;
A10:
for y being object st y in REAL holds
ex x being object st
( x in REAL 1 & y = (proj (1,1)) . x )
then
rng (proj (1,1)) = REAL
by FUNCT_2:10;
then
proj (1,1) is onto
by FUNCT_2:def 3;
hence
( proj (1,1) is bijective & dom (proj (1,1)) = REAL 1 & rng (proj (1,1)) = REAL & ( for x being Real holds
( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> ) ) )
by A6, A10, A8, FUNCT_2:10, FUNCT_2:def 1; verum