let d be non zero Nat; :: thesis: for x being Element of REAL d holds cell (x,x) = {x}

let x be Element of REAL d; :: thesis: cell (x,x) = {x}

for x9 being object holds

( x9 in cell (x,x) iff x9 = x )

let x be Element of REAL d; :: thesis: cell (x,x) = {x}

for x9 being object holds

( x9 in cell (x,x) iff x9 = x )

proof

hence
cell (x,x) = {x}
by TARSKI:def 1; :: thesis: verum
let x9 be object ; :: thesis: ( x9 in cell (x,x) iff x9 = x )

thus ( x9 in cell (x,x) implies x9 = x ) :: thesis: ( x9 = x implies x9 in cell (x,x) )

end;thus ( x9 in cell (x,x) implies x9 = x ) :: thesis: ( x9 = x implies x9 in cell (x,x) )

proof

thus
( x9 = x implies x9 in cell (x,x) )
by Th23; :: thesis: verum
assume A1:
x9 in cell (x,x)
; :: thesis: x9 = x

then reconsider x = x, x9 = x9 as Function of (Seg d),REAL by Def3;

end;then reconsider x = x, x9 = x9 as Function of (Seg d),REAL by Def3;

now :: thesis: for i being Element of Seg d holds x9 . i = x . i

hence
x9 = x
by FUNCT_2:63; :: thesis: verumlet i be Element of Seg d; :: thesis: x9 . i = x . i

A2: for i being Element of Seg d holds x . i <= x . i ;

then A3: x . i <= x9 . i by A1, Th21;

x9 . i <= x . i by A1, A2, Th21;

hence x9 . i = x . i by A3, XXREAL_0:1; :: thesis: verum

end;A2: for i being Element of Seg d holds x . i <= x . i ;

then A3: x . i <= x9 . i by A1, Th21;

x9 . i <= x . i by A1, A2, Th21;

hence x9 . i = x . i by A3, XXREAL_0:1; :: thesis: verum