let x, y be Element of REAL 1; :: thesis: (Infty_dist 1) . (x,y) = |.((x . 1) - (y . 1)).|
consider S being ext-real-membered set such that
A1: S = { |.((x . i) - (y . i)).| where i is Element of Seg 1 : verum } and
A2: (Infty_dist 1) . (x,y) = sup S by Th57;
S = {|.((x . 1) - (y . 1)).|}
proof
for t being object st t in S holds
t in {|.((x . 1) - (y . 1)).|}
proof
let t be object ; :: thesis: ( t in S implies t in {|.((x . 1) - (y . 1)).|} )
assume t in S ; :: thesis: t in {|.((x . 1) - (y . 1)).|}
then consider i being Element of Seg 1 such that
A3: t = |.((x . i) - (y . i)).| by A1;
i = 1 by TARSKI:def 1, FINSEQ_1:2;
hence t in {|.((x . 1) - (y . 1)).|} by A3, TARSKI:def 1; :: thesis: verum
end;
then A4: S c= {|.((x . 1) - (y . 1)).|} ;
for t being object st t in {|.((x . 1) - (y . 1)).|} holds
t in S
proof
let t be object ; :: thesis: ( t in {|.((x . 1) - (y . 1)).|} implies t in S )
assume t in {|.((x . 1) - (y . 1)).|} ; :: thesis: t in S
then A5: t = |.((x . 1) - (y . 1)).| by TARSKI:def 1;
1 is Element of Seg 1 by TARSKI:def 1, FINSEQ_1:2;
hence t in S by A5, A1; :: thesis: verum
end;
then {|.((x . 1) - (y . 1)).|} c= S ;
hence S = {|.((x . 1) - (y . 1)).|} by A4; :: thesis: verum
end;
hence (Infty_dist 1) . (x,y) = |.((x . 1) - (y . 1)).| by A2, XXREAL_2:11; :: thesis: verum