let m be non zero Nat; for f being PartFunc of (REAL m),REAL
for x, y being Element of REAL m
for i being Nat
for xi being Real st 1 <= i & i <= m & y = (reproj (i,x)) . xi holds
reproj (i,x) = reproj (i,y)
let f be PartFunc of (REAL m),REAL; for x, y being Element of REAL m
for i being Nat
for xi being Real st 1 <= i & i <= m & y = (reproj (i,x)) . xi holds
reproj (i,x) = reproj (i,y)
let x, y be Element of REAL m; for i being Nat
for xi being Real st 1 <= i & i <= m & y = (reproj (i,x)) . xi holds
reproj (i,x) = reproj (i,y)
let i be Nat; for xi being Real st 1 <= i & i <= m & y = (reproj (i,x)) . xi holds
reproj (i,x) = reproj (i,y)
let xi be Real; ( 1 <= i & i <= m & y = (reproj (i,x)) . xi implies reproj (i,x) = reproj (i,y) )
reconsider xx = xi as Element of REAL by XREAL_0:def 1;
assume A1:
( 1 <= i & i <= m & y = (reproj (i,x)) . xi )
; reproj (i,x) = reproj (i,y)
then A2:
y = Replace (x,i,xx)
by PDIFF_1:def 5;
A3:
( len x = m & len y = m )
by CARD_1:def 7;
then A4:
y = ((x | (i -' 1)) ^ <*xi*>) ^ (x /^ i)
by A1, A2, FINSEQ_7:def 1;
A5: dom (reproj (i,x)) =
REAL
by PDIFF_1:def 5
.=
dom (reproj (i,y))
by PDIFF_1:def 5
;
for r being object st r in dom (reproj (i,x)) holds
(reproj (i,x)) . r = (reproj (i,y)) . r
proof
let r be
object ;
( r in dom (reproj (i,x)) implies (reproj (i,x)) . r = (reproj (i,y)) . r )
assume A6:
r in dom (reproj (i,x))
;
(reproj (i,x)) . r = (reproj (i,y)) . r
A7:
(
i -' 1
<= len y &
i -' 1
<= len x )
by A1, A3, NAT_D:44;
reconsider r1 =
r as
Element of
REAL by A6;
(reproj (i,x)) . r = Replace (
x,
i,
r1)
by PDIFF_1:def 5;
then A8:
(reproj (i,x)) . r = ((x | (i -' 1)) ^ <*r1*>) ^ (x /^ i)
by A1, A3, FINSEQ_7:def 1;
(reproj (i,y)) . r = Replace (
y,
i,
r1)
by PDIFF_1:def 5;
then A9:
(reproj (i,y)) . r = ((y | (i -' 1)) ^ <*r1*>) ^ (y /^ i)
by A1, A3, FINSEQ_7:def 1;
A10:
dom (y | (i -' 1)) = Seg (i -' 1)
by A7, FINSEQ_1:17;
then A11:
dom (y | (i -' 1)) = dom (x | (i -' 1))
by A7, FINSEQ_1:17;
A12:
for
n being
Nat st
n in dom (y | (i -' 1)) holds
(y | (i -' 1)) /. n = (x | (i -' 1)) /. n
proof
let n be
Nat;
( n in dom (y | (i -' 1)) implies (y | (i -' 1)) /. n = (x | (i -' 1)) /. n )
assume A13:
n in dom (y | (i -' 1))
;
(y | (i -' 1)) /. n = (x | (i -' 1)) /. n
then
n in Seg (len (x | (i -' 1)))
by A7, A10, FINSEQ_1:17;
then A14:
n <= len (x | (i -' 1))
by FINSEQ_1:1;
A15:
len (x | (i -' 1)) <= i -' 1
by FINSEQ_5:17;
A16:
( 1
<= n &
n <= len (x | (i -' 1)) )
by A13, A11, FINSEQ_3:25;
(y | (i -' 1)) /. n =
(y | (i -' 1)) . n
by A13, PARTFUN1:def 6
.=
(((x | (i -' 1)) ^ <*xi*>) ^ (x /^ i)) . n
by A4, A15, A14, FINSEQ_3:112, XXREAL_0:2
.=
((x | (i -' 1)) ^ (<*xi*> ^ (x /^ i))) . n
by FINSEQ_1:32
.=
(x | (i -' 1)) . n
by A16, FINSEQ_1:64
.=
(x | (i -' 1)) /. n
by A13, A11, PARTFUN1:def 6
;
hence
(y | (i -' 1)) /. n = (x | (i -' 1)) /. n
;
verum
end;
A17:
(
len (y /^ i) = (len y) -' i &
len (x /^ i) = (len x) -' i )
by RFINSEQ:29;
for
n being
Nat st 1
<= n &
n <= len (y /^ i) holds
(y /^ i) . n = (x /^ i) . n
proof
let n be
Nat;
( 1 <= n & n <= len (y /^ i) implies (y /^ i) . n = (x /^ i) . n )
assume A18:
( 1
<= n &
n <= len (y /^ i) )
;
(y /^ i) . n = (x /^ i) . n
then A19:
(
n in dom (y /^ i) &
n in dom (x /^ i) )
by A17, A3, FINSEQ_3:25;
A20:
len (x | (i -' 1)) = i -' 1
by A1, A3, FINSEQ_1:59, NAT_D:44;
A21:
len <*xi*> = 1
by FINSEQ_1:39;
i - 1
>= 0
by A1, XREAL_1:48;
then
i -' 1
= i - 1
by XREAL_0:def 2;
then A22:
len ((x | (i -' 1)) ^ <*xi*>) =
(i - 1) + 1
by A20, A21, FINSEQ_1:22
.=
i
;
(y /^ i) . n =
y . (i + n)
by A19, FINSEQ_7:4
.=
(x /^ i) . n
by A18, A4, A22, FINSEQ_1:65
;
hence
(y /^ i) . n = (x /^ i) . n
;
verum
end;
then
y /^ i = x /^ i
by A17, A3;
hence
(reproj (i,x)) . r = (reproj (i,y)) . r
by A8, A9, A11, A12, FINSEQ_5:12;
verum
end;
hence
reproj (i,x) = reproj (i,y)
by A5, FUNCT_1:2; verum