let n be Nat; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( d is_a_unity_wrt B implies n |-> d is_a_unity_wrt product (B,n) )

assume d is_a_unity_wrt B ; :: thesis: 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;

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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( d is_a_unity_wrt B implies n |-> d is_a_unity_wrt product (B,n) )

assume d is_a_unity_wrt B ; :: thesis: 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 :: thesis: for b being Element of n -tuples_on D holds

( (product (B,n)) . ((n |-> d),b) = b & (product (B,n)) . (b,(n |-> d)) = b )

hence
n |-> d is_a_unity_wrt product (B,n)
by BINOP_1:3; :: thesis: verum( (product (B,n)) . ((n |-> d),b) = b & (product (B,n)) . (b,(n |-> d)) = b )

let b be Element of n -tuples_on D; :: thesis: ( (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 ; :: thesis: (product (B,n)) . (b,(n |-> d)) = b

thus (product (B,n)) . (b,(n |-> d)) = B .: (b9,(n |-> d)) by Def1

.= b by A1, FINSEQOP:56 ; :: thesis: verum

end;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 ; :: thesis: (product (B,n)) . (b,(n |-> d)) = b

thus (product (B,n)) . (b,(n |-> d)) = B .: (b9,(n |-> d)) by Def1

.= b by A1, FINSEQOP:56 ; :: thesis: verum