set F = Solutions_of_Sierp168 f;
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 (Solutions_of_Sierp168 f) or not x2 in proj1 (Solutions_of_Sierp168 f) or not (Solutions_of_Sierp168 f) . x1 = (Solutions_of_Sierp168 f) . x2 or x1 = x2 )
assume ( x1 in dom (Solutions_of_Sierp168 f) & x2 in dom (Solutions_of_Sierp168 f) ) ; :: thesis: ( not (Solutions_of_Sierp168 f) . x1 = (Solutions_of_Sierp168 f) . x2 or x1 = x2 )
then reconsider x1 = x1, x2 = x2 as Element of NATPLUS ;
( (Solutions_of_Sierp168 f) . x1 = x1 (#) f & (Solutions_of_Sierp168 f) . x2 = x2 (#) f ) by Def15;
hence ( not (Solutions_of_Sierp168 f) . x1 = (Solutions_of_Sierp168 f) . x2 or x1 = x2 ) by VALUED_2:9; :: thesis: verum