set f = prodnorm ;

A1: for a, b being Element of [.0,1.] holds prodnorm . (a,b) = prodnorm . (b,a)

prodnorm . (a,b) <= prodnorm . (c,d)

for a being Element of [.0,1.] holds prodnorm . (a,1) = a

A1: for a, b being Element of [.0,1.] holds prodnorm . (a,b) = prodnorm . (b,a)

proof

C1:
for a, b, c being Element of [.0,1.] holds prodnorm . ((prodnorm . (a,b)),c) = prodnorm . (a,(prodnorm . (b,c)))
let a, b be Element of [.0,1.]; :: thesis: prodnorm . (a,b) = prodnorm . (b,a)

prodnorm . (a,b) = a * b by ProdDef

.= prodnorm . (b,a) by ProdDef ;

hence prodnorm . (a,b) = prodnorm . (b,a) ; :: thesis: verum

end;prodnorm . (a,b) = a * b by ProdDef

.= prodnorm . (b,a) by ProdDef ;

hence prodnorm . (a,b) = prodnorm . (b,a) ; :: thesis: verum

proof

D1:
for a, b, c, d being Element of [.0,1.] st a <= c & b <= d holds
let a, b, c be Element of [.0,1.]; :: thesis: prodnorm . ((prodnorm . (a,b)),c) = prodnorm . (a,(prodnorm . (b,c)))

A2: a * b in [.0,1.] by Lemma1;

A3: b * c in [.0,1.] by Lemma1;

prodnorm . ((prodnorm . (a,b)),c) = prodnorm . ((a * b),c) by ProdDef

.= (a * b) * c by ProdDef, A2

.= a * (b * c)

.= prodnorm . (a,(b * c)) by A3, ProdDef

.= prodnorm . (a,(prodnorm . (b,c))) by ProdDef ;

hence prodnorm . ((prodnorm . (a,b)),c) = prodnorm . (a,(prodnorm . (b,c))) ; :: thesis: verum

end;A2: a * b in [.0,1.] by Lemma1;

A3: b * c in [.0,1.] by Lemma1;

prodnorm . ((prodnorm . (a,b)),c) = prodnorm . ((a * b),c) by ProdDef

.= (a * b) * c by ProdDef, A2

.= a * (b * c)

.= prodnorm . (a,(b * c)) by A3, ProdDef

.= prodnorm . (a,(prodnorm . (b,c))) by ProdDef ;

hence prodnorm . ((prodnorm . (a,b)),c) = prodnorm . (a,(prodnorm . (b,c))) ; :: thesis: verum

prodnorm . (a,b) <= prodnorm . (c,d)

proof

T1:
1 in [.0,1.]
by XXREAL_1:1;
let a, b, c, d be Element of [.0,1.]; :: thesis: ( a <= c & b <= d implies prodnorm . (a,b) <= prodnorm . (c,d) )

B1: ( 0 <= a & 0 <= b ) by XXREAL_1:1;

assume ( a <= c & b <= d ) ; :: thesis: prodnorm . (a,b) <= prodnorm . (c,d)

then a * b <= c * d by B1, XREAL_1:66;

then a * b <= prodnorm . (c,d) by ProdDef;

hence prodnorm . (a,b) <= prodnorm . (c,d) by ProdDef; :: thesis: verum

end;B1: ( 0 <= a & 0 <= b ) by XXREAL_1:1;

assume ( a <= c & b <= d ) ; :: thesis: prodnorm . (a,b) <= prodnorm . (c,d)

then a * b <= c * d by B1, XREAL_1:66;

then a * b <= prodnorm . (c,d) by ProdDef;

hence prodnorm . (a,b) <= prodnorm . (c,d) by ProdDef; :: thesis: verum

for a being Element of [.0,1.] holds prodnorm . (a,1) = a

proof

hence
( prodnorm is commutative & prodnorm is associative & prodnorm is monotonic & prodnorm is with-1-identity )
by BINOP_1:def 2, BINOP_1:def 3, A1, C1, D1; :: thesis: verum
let a be Element of [.0,1.]; :: thesis: prodnorm . (a,1) = a

a * 1 = a ;

hence prodnorm . (a,1) = a by ProdDef, T1; :: thesis: verum

end;a * 1 = a ;

hence prodnorm . (a,1) = a by ProdDef, T1; :: thesis: verum