set X = {0,1,2};

XX: 0 in {0,1,2} by ENUMSET1:def 1;

set f = QLT_Ex1 ;

thus QLT_Ex1 is commutative :: thesis: ( QLT_Ex1 is associative & QLT_Ex1 is idempotent )

thus QLT_Ex1 . (a,a) = a by QLTEx1Def; :: thesis: verum

XX: 0 in {0,1,2} by ENUMSET1:def 1;

set f = QLT_Ex1 ;

thus QLT_Ex1 is commutative :: thesis: ( QLT_Ex1 is associative & QLT_Ex1 is idempotent )

proof

thus
QLT_Ex1 is associative
:: thesis: QLT_Ex1 is idempotent
let a, b be Element of {0,1,2}; :: according to BINOP_1:def 2 :: thesis: QLT_Ex1 . (a,b) = QLT_Ex1 . (b,a)

end;proof

let a be Element of {0,1,2}; :: according to BINOP_1:def 4 :: thesis: QLT_Ex1 . (a,a) = a
let a, b, c be Element of {0,1,2}; :: according to BINOP_1:def 3 :: thesis: QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c)

end;per cases
( ( a = b & b = c ) or ( a <> b & b = c ) or ( a = b & b <> c ) or ( a <> b & b <> c ) )
;

end;

suppose A1:
( a = b & b = c )
; :: thesis: QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c)

then
QLT_Ex1 . (a,b) = a
by QLTEx1Def;

hence QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c) by A1; :: thesis: verum

end;hence QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c) by A1; :: thesis: verum

suppose A1:
( a <> b & b = c )
; :: thesis: QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c)

then A2:
QLT_Ex1 . (a,b) = 0
by QLTEx1Def;

D2: 0 in {0,1,2} by ENUMSET1:def 1;

QLT_Ex1 . ((QLT_Ex1 . (a,b)),c) = QLT_Ex1 . (0,c) by A1, QLTEx1Def

.= 0 by QLTEx1Def, D2 ;

hence QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c) by A2, QLTEx1Def, A1; :: thesis: verum

end;D2: 0 in {0,1,2} by ENUMSET1:def 1;

QLT_Ex1 . ((QLT_Ex1 . (a,b)),c) = QLT_Ex1 . (0,c) by A1, QLTEx1Def

.= 0 by QLTEx1Def, D2 ;

hence QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c) by A2, QLTEx1Def, A1; :: thesis: verum

suppose A1:
( a = b & b <> c )
; :: thesis: QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c)

then A2:
QLT_Ex1 . (a,b) = a
by QLTEx1Def;

A3: QLT_Ex1 . (b,c) = 0 by QLTEx1Def, A1;

end;A3: QLT_Ex1 . (b,c) = 0 by QLTEx1Def, A1;

suppose A1:
( a <> b & b <> c )
; :: thesis: QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c)

then A3:
QLT_Ex1 . (b,c) = 0
by QLTEx1Def;

end;per cases
( a = 0 or a <> 0 )
;

end;

suppose B1:
a = 0
; :: thesis: QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c)

QLT_Ex1 . ((QLT_Ex1 . (a,b)),c) =
QLT_Ex1 . (0,c)
by A1, QLTEx1Def

.= 0 by B1, QLTEx1Def ;

hence QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c) by B1, QLTEx1Def, A3; :: thesis: verum

end;.= 0 by B1, QLTEx1Def ;

hence QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c) by B1, QLTEx1Def, A3; :: thesis: verum

suppose b1:
a <> 0
; :: thesis: QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c)

QLT_Ex1 . ((QLT_Ex1 . (a,b)),c) =
QLT_Ex1 . (0,c)
by A1, QLTEx1Def

.= 0 by QLTEx1Def, XX ;

hence QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c) by b1, QLTEx1Def, A3; :: thesis: verum

end;.= 0 by QLTEx1Def, XX ;

hence QLT_Ex1 . (a,(QLT_Ex1 . (b,c))) = QLT_Ex1 . ((QLT_Ex1 . (a,b)),c) by b1, QLTEx1Def, A3; :: thesis: verum

thus QLT_Ex1 . (a,a) = a by QLTEx1Def; :: thesis: verum