let N1, N2 be Fuzzy_Negation; :: thesis: ( N1 ~ = N2 implies N1 is onto )
assume N1 ~ = N2 ; :: thesis: N1 is onto
then AB: N1 = N2 ~ ;
then FF: N2 is one-to-one by LemmaOne;
for y being object st y in [.0,1.] holds
ex x being object st
( x in [.0,1.] & y = N1 . x )

proof

let y be object ; :: thesis: ( y in [.0,1.] implies ex x being object st
( x in [.0,1.] & y = N1 . x ) )
assume A2: y in [.0,1.] ; :: thesis: ex x being object st
( x in [.0,1.] & y = N1 . x )
take x = N2 . y; :: thesis: ( x in [.0,1.] & y = N1 . x )
N1 = N2 " by AB, LemmaOne, FUNCT_1:def 5;
hence ( x in [.0,1.] & y = N1 . x ) by A2, FF, FUNCT_2:26, FUNCT_2:5; :: thesis: verum

end;

then rng N1 = [.0,1.] by FUNCT_2:10;
hence N1 is onto by FUNCT_2:def 3; :: thesis: verum