let n be non zero Nat; :: thesis: for x, y being Element of REAL n holds
( { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } is real-membered & { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } = rng (abs (x - y)) )
let x, y be Element of REAL n; :: thesis: ( { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } is real-membered & { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } = rng (abs (x - y)) )
set SA = { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } ;
now :: thesis: for t being object st t in { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } holds
t is real
let t be object ; :: thesis: ( t in { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } implies t is real )
assume t in { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } ; :: thesis: t is real
then ex i being Element of Seg n st t = |.((x . i) - (y . i)).| ;
hence t is real ; :: thesis: verum
end;
hence { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } is real-membered by MEMBERED:def 3; :: thesis: { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } = rng (abs (x - y))
A1: { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } c= rng (abs (x - y))
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } or t in rng (abs (x - y)) )
assume t in { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } ; :: thesis: t in rng (abs (x - y))
then consider i being Element of Seg n such that
A2: t = |.((x . i) - (y . i)).| ;
A3: ( t = |.((x - y) . i).| & dom (abs (x - y)) = Seg n ) by A2, RVSUM_1:27, FINSEQ_2:124;
reconsider f = x - y as complex-valued Function ;
t = |.f.| . i by A3, VALUED_1:18;
hence t in rng (abs (x - y)) by A3, FUNCT_1:def 3; :: thesis: verum
end;
for t being object st t in rng (abs (x - y)) holds
t in { |.((x . i) - (y . i)).| where i is Element of Seg n : verum }
proof
let t be object ; :: thesis: ( t in rng (abs (x - y)) implies t in { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } )
assume t in rng (abs (x - y)) ; :: thesis: t in { |.((x . i) - (y . i)).| where i is Element of Seg n : verum }
then consider i being object such that
A4: i in dom (abs (x - y)) and
A5: t = (abs (x - y)) . i by FUNCT_1:def 3;
A6: i is Element of Seg n by A4, FINSEQ_2:124;
reconsider f = x - y as complex-valued Function ;
( t = |.((x - y) . i).| & (x - y) . i = (x . i) - (y . i) ) by A4, A5, VALUED_1:18, RVSUM_1:27;
hence t in { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } by A6; :: thesis: verum
end;
then rng (abs (x - y)) c= { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } ;
hence { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } = rng (abs (x - y)) by A1; :: thesis: verum