:: BINARITH semantic presentation

begin

theorem Th1: :: BINARITH:1
for i, n being Nat
for D being non empty set
for d being Element of D
for z being Tuple of n,D st i in Seg n holds
(z ^ <*d*>) /. i = z /. i
proof
let i, n be Nat; ::_thesis: for D being non empty set
for d being Element of D
for z being Tuple of n,D st i in Seg n holds
(z ^ <*d*>) /. i = z /. i
let D be non empty set ; ::_thesis: for d being Element of D
for z being Tuple of n,D st i in Seg n holds
(z ^ <*d*>) /. i = z /. i
let d be Element of D; ::_thesis: for z being Tuple of n,D st i in Seg n holds
(z ^ <*d*>) /. i = z /. i
let z be Tuple of n,D; ::_thesis: ( i in Seg n implies (z ^ <*d*>) /. i = z /. i )
assume A1: i in Seg n ; ::_thesis: (z ^ <*d*>) /. i = z /. i
 len z = n by CARD_1:def_7;
end;