:: 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 set st i in dom b₃ holds
for f, g being FinSequence st f = F . i & g = G . i holds
b₃ . i = f ^ g ) ) );