let n be Nat; for D being non empty set
for d being Element of D
for B being BinOp of D st d is_a_unity_wrt B holds
n |-> d is_a_unity_wrt product (B,n)
let D be non empty set ; for d being Element of D
for B being BinOp of D st d is_a_unity_wrt B holds
n |-> d is_a_unity_wrt product (B,n)
let d be Element of D; for B being BinOp of D st d is_a_unity_wrt B holds
n |-> d is_a_unity_wrt product (B,n)
let B be BinOp of D; ( d is_a_unity_wrt B implies n |-> d is_a_unity_wrt product (B,n) )
assume
d is_a_unity_wrt B
; n |-> d is_a_unity_wrt product (B,n)
then A1:
( B is having_a_unity & d = the_unity_wrt B )
by BINOP_1:def 8, SETWISEO:def 2;
now for b being Element of n -tuples_on D holds
( (product (B,n)) . ((n |-> d),b) = b & (product (B,n)) . (b,(n |-> d)) = b )let b be
Element of
n -tuples_on D;
( (product (B,n)) . ((n |-> d),b) = b & (product (B,n)) . (b,(n |-> d)) = b )reconsider b9 =
b as
Element of
n -tuples_on D ;
thus (product (B,n)) . (
(n |-> d),
b) =
B .: (
(n |-> d),
b9)
by Def1
.=
b
by A1, FINSEQOP:56
;
(product (B,n)) . (b,(n |-> d)) = bthus (product (B,n)) . (
b,
(n |-> d)) =
B .: (
b9,
(n |-> d))
by Def1
.=
b
by A1, FINSEQOP:56
;
verum end;
hence
n |-> d is_a_unity_wrt product (B,n)
by BINOP_1:3; verum