let I be BinOp of [.0,1.]; :: thesis: for N being negation-strict Fuzzy_Negation
for N1 being Fuzzy_Negation st N ~ = N1 holds
( I is N -satisfying_L-CP iff I is N1 -satisfying_R-CP )
let N be negation-strict Fuzzy_Negation; :: thesis: for N1 being Fuzzy_Negation st N ~ = N1 holds
( I is N -satisfying_L-CP iff I is N1 -satisfying_R-CP )
let N1 be Fuzzy_Negation; :: thesis: ( N ~ = N1 implies ( I is N -satisfying_L-CP iff I is N1 -satisfying_R-CP ) )
assume A0: N ~ = N1 ; :: thesis: ( I is N -satisfying_L-CP iff I is N1 -satisfying_R-CP )
then N is onto by LemmaOnto2;
then A2: rng N = [.0,1.] by FUNCT_2:def 3;
DD: N " = N ~ by FUNCT_1:def 5;
thus ( I is N -satisfying_L-CP implies I is N1 -satisfying_R-CP ) :: thesis: ( I is N1 -satisfying_R-CP implies I is N -satisfying_L-CP )

proof

assume a1: I is N -satisfying_L-CP ; :: thesis: I is N1 -satisfying_R-CP
for x, y being Element of [.0,1.] holds I . (x,(N1 . y)) = I . (y,(N1 . x))

proof

let x, y be Element of [.0,1.]; :: thesis: I . (x,(N1 . y)) = I . (y,(N1 . x))
I . (x,(N1 . y)) = I . ((N . (N1 . x)),(N1 . y)) by A0, A2, FUNCT_1:35, DD
.= I . ((N . (N1 . y)),(N1 . x)) by a1
.= I . (y,(N1 . x)) by A2, DD, A0, FUNCT_1:35 ;
hence I . (x,(N1 . y)) = I . (y,(N1 . x)) ; :: thesis: verum

end;

hence I is N1 -satisfying_R-CP ; :: thesis: verum

end;

assume a1: I is N1 -satisfying_R-CP ; :: thesis: I is N -satisfying_L-CP
C1: dom N = [.0,1.] by FUNCT_2:def 1;
for x, y being Element of [.0,1.] holds I . ((N . x),y) = I . ((N . y),x)

proof

let x, y be Element of [.0,1.]; :: thesis: I . ((N . x),y) = I . ((N . y),x)
B2: (N1 * N) . y = y by A0, C1, FUNCT_1:34, DD;
(N1 * N) . y = N1 . (N . y) by C1, FUNCT_1:13;
then I . ((N . x),y) = I . ((N . y),(N1 . (N . x))) by a1, B2
.= I . ((N . y),x) by A0, C1, FUNCT_1:34, DD ;
hence I . ((N . x),y) = I . ((N . y),x) ; :: thesis: verum

end;

hence I is N -satisfying_L-CP ; :: thesis: verum