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;

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 )

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;

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