let p be FinSequence; :: thesis: for x being object st x in rng p holds
( x .. p = 1 iff p -| x = {} )
let x be object ; :: thesis: ( x in rng p implies ( x .. p = 1 iff p -| x = {} ) )
assume A1: x in rng p ; :: thesis: ( x .. p = 1 iff p -| x = {} )
thus ( x .. p = 1 implies p -| x = {} ) :: thesis: ( p -| x = {} implies x .. p = 1 )
proof
assume A2: x .. p = 1 ; :: thesis: p -| x = {}
len (p -| x) = (x .. p) - 1 by A1, Th34
.= 0 by A2 ;
hence p -| x = {} ; :: thesis: verum
end;
assume p -| x = {} ; :: thesis: x .. p = 1
then A3: len (p -| x) = 0 ;
len (p -| x) = (x .. p) - 1 by A1, Th34;
hence x .. p = 1 by A3; :: thesis: verum