[Date Prev][Date Next] [Chronological] [Thread] [Top]

[mizar] A question

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;


-- 
Piotr Rudnicki              CompSci, University of Alberta, Edmonton, Canada
http://web.cs.ualberta.ca/~piotr