:: deftheorem Def4 defines ^^ PRE_POLY:def 4 :
for F, G being FinSequence-yielding Function
for b₃ being Function holds
( b₃ = F ^^ G iff ( dom b₃ = (dom F) /\ (dom G) & ( for i being object st i in dom b₃ holds
b₃ . i = (F . i) ^ (G . i) ) ) );