let p be FinSequence; :: thesis: for x being set holds
( p just_once_values x iff len (p - {x}) = (len p) - 1 )
let x be set ; :: thesis: ( p just_once_values x iff len (p - {x}) = (len p) - 1 )
thus ( p just_once_values x implies len (p - {x}) = (len p) - 1 ) :: thesis: ( len (p - {x}) = (len p) - 1 implies p just_once_values x )

proof

assume A1: p just_once_values x ; :: thesis: len (p - {x}) = (len p) - 1
A2: len (p - {x}) = (len p) - (card (p " {x})) by FINSEQ_3:66;
p " {x} = {(x .. p)} by A1, Th38;
hence len (p - {x}) = (len p) - 1 by A2, CARD_1:50; :: thesis: verum

end;

assume len (p - {x}) = (len p) - 1 ; :: thesis: p just_once_values x
then (len p) + (- 1) = (len p) - (card (p " {x})) by FINSEQ_3:66
.= (len p) + (- (card (p " {x}))) ;
hence p just_once_values x by Def2; :: thesis: verum