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

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:57 ; :: 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:57 ; :: thesis: verum

end;

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