Re: [mizar] A question

[Grzegorz Bancerek <bancerek@math.uwb.edu.pl>]

Piotr Rudnicki wrote:
> Hi:
>
> I am puzzled by the following:
>
> now
>   let X be set;
>   consider Y being set such that
> A: X = Y;
>   consider f being FinSequence of X;
>   reconsider g = f as FinSequence of Y by A;
>   g = f;
>   g/.1 = f/.1;
> ::>         *4
>   g.1 = f.1;
> end;
Hi,

/. has two arguments, so in your example "by A" should
be added.  What about this:

environ
 vocabulary BOOLE,FINSEQ_1,FINSEQ_4;
 constructors TARSKI, SUBSET_1, FINSEQ_1, FINSEQ_4;
 notation TARSKI, XBOOLE_0, FINSEQ_1, FINSEQ_4;
 clusters SUBSET_1, FINSEQ_1;
 theorems FINSEQ_1, TARSKI;
 requirements BOOLE,SUBSET;
begin

now
  set X = { 0 };
  set Y = { 1 };
  set f = <*> X;
  <*> Y = {} by FINSEQ_1:def 6 .= f by FINSEQ_1:def 6; then
  reconsider g = f as FinSequence of Y;
  g/.1 = 1 & f/.1 = 0 by TARSKI:def 1;
then
  g/.1 <> f/.1;
end;

Grzegorz