let S1 be OrderSortedSign; :: thesis: for U1 being OSAlgebra of S1 holds

( U1 is monotone iff MSAlgebra(# the Sorts of U1, the Charact of U1 #) is monotone )

let U1 be OSAlgebra of S1; :: thesis: ( U1 is monotone iff MSAlgebra(# the Sorts of U1, the Charact of U1 #) is monotone )

set U2 = MSAlgebra(# the Sorts of U1, the Charact of U1 #);

let o1, o2 be OperSymbol of S1; :: according to OSALG_1:def 21 :: thesis: ( not o1 <= o2 or (Den (o2,U1)) | (Args (o1,U1)) = Den (o1,U1) )

assume o1 <= o2 ; :: thesis: (Den (o2,U1)) | (Args (o1,U1)) = Den (o1,U1)

then A5: (Den (o2,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) | (Args (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) = Den (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) by A4;

thus (Den (o2,U1)) | (Args (o1,U1)) = (Den (o2,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) | (Args (o1,U1)) by A1

.= Den (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) by A1, A5

.= Den (o1,U1) by A1 ; :: thesis: verum

( U1 is monotone iff MSAlgebra(# the Sorts of U1, the Charact of U1 #) is monotone )

let U1 be OSAlgebra of S1; :: thesis: ( U1 is monotone iff MSAlgebra(# the Sorts of U1, the Charact of U1 #) is monotone )

set U2 = MSAlgebra(# the Sorts of U1, the Charact of U1 #);

A1: now :: thesis: for o1 being OperSymbol of S1 holds

( Den (o1,U1) = Den (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) & Args (o1,U1) = Args (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) )

thus
( U1 is monotone implies MSAlgebra(# the Sorts of U1, the Charact of U1 #) is monotone )
:: thesis: ( MSAlgebra(# the Sorts of U1, the Charact of U1 #) is monotone implies U1 is monotone )( Den (o1,U1) = Den (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) & Args (o1,U1) = Args (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) )

let o1 be OperSymbol of S1; :: thesis: ( Den (o1,U1) = Den (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) & Args (o1,U1) = Args (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) )

thus Den (o1,U1) = the Charact of MSAlgebra(# the Sorts of U1, the Charact of U1 #) . o1 by MSUALG_1:def 6

.= Den (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) by MSUALG_1:def 6 ; :: thesis: Args (o1,U1) = Args (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))

thus Args (o1,U1) = (( the Sorts of MSAlgebra(# the Sorts of U1, the Charact of U1 #) #) * the Arity of S1) . o1 by MSUALG_1:def 4

.= Args (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) by MSUALG_1:def 4 ; :: thesis: verum

end;thus Den (o1,U1) = the Charact of MSAlgebra(# the Sorts of U1, the Charact of U1 #) . o1 by MSUALG_1:def 6

.= Den (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) by MSUALG_1:def 6 ; :: thesis: Args (o1,U1) = Args (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))

thus Args (o1,U1) = (( the Sorts of MSAlgebra(# the Sorts of U1, the Charact of U1 #) #) * the Arity of S1) . o1 by MSUALG_1:def 4

.= Args (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) by MSUALG_1:def 4 ; :: thesis: verum

proof

assume A4:
MSAlgebra(# the Sorts of U1, the Charact of U1 #) is monotone
; :: thesis: U1 is monotone
assume A2:
U1 is monotone
; :: thesis: MSAlgebra(# the Sorts of U1, the Charact of U1 #) is monotone

let o1, o2 be OperSymbol of S1; :: according to OSALG_1:def 21 :: thesis: ( not o1 <= o2 or (Den (o2,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) | (Args (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) = Den (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) )

assume o1 <= o2 ; :: thesis: (Den (o2,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) | (Args (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) = Den (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))

then A3: (Den (o2,U1)) | (Args (o1,U1)) = Den (o1,U1) by A2;

thus (Den (o2,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) | (Args (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) = (Den (o2,U1)) | (Args (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) by A1

.= Den (o1,U1) by A1, A3

.= Den (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) by A1 ; :: thesis: verum

end;let o1, o2 be OperSymbol of S1; :: according to OSALG_1:def 21 :: thesis: ( not o1 <= o2 or (Den (o2,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) | (Args (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) = Den (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) )

assume o1 <= o2 ; :: thesis: (Den (o2,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) | (Args (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) = Den (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))

then A3: (Den (o2,U1)) | (Args (o1,U1)) = Den (o1,U1) by A2;

thus (Den (o2,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) | (Args (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) = (Den (o2,U1)) | (Args (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) by A1

.= Den (o1,U1) by A1, A3

.= Den (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) by A1 ; :: thesis: verum

let o1, o2 be OperSymbol of S1; :: according to OSALG_1:def 21 :: thesis: ( not o1 <= o2 or (Den (o2,U1)) | (Args (o1,U1)) = Den (o1,U1) )

assume o1 <= o2 ; :: thesis: (Den (o2,U1)) | (Args (o1,U1)) = Den (o1,U1)

then A5: (Den (o2,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) | (Args (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) = Den (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) by A4;

thus (Den (o2,U1)) | (Args (o1,U1)) = (Den (o2,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) | (Args (o1,U1)) by A1

.= Den (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) by A1, A5

.= Den (o1,U1) by A1 ; :: thesis: verum