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 p just_once_values x ; :: thesis: len (p - {x}) = (len p) - 1
then ( len (p - {x}) = (len p) - (card (p " {x})) & p " {x} = {(x .. p)} ) by Th38, FINSEQ_3:59;
hence len (p - {x}) = (len p) - 1 by CARD_1:30; :: 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:59
.= (len p) + (- (card (p " {x}))) ;
hence p just_once_values x by Def2; :: thesis: verum