let p be FinSequence; :: thesis: for x being object holds
( p just_once_values x iff len (p - {x}) = (len p) - 1 )
let x be object ; :: 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 ) by FINSEQ_3:59; :: thesis: ( len (p - {x}) = (len p) - 1 implies p just_once_values x )
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 ; :: thesis: verum