:: deftheorem Def42 defines extendWith FOMODEL1:def 42 :
for f being INT -valued Function
for L being non empty Language-like
for b₃ being non empty strict Language-like holds
( b₃ = L extendWith f iff ( the adicity of b₃ = (f | ((dom f) \ { the OneF of L})) +* the adicity of L & the ZeroF of b₃ = the ZeroF of L & the OneF of b₃ = the OneF of L ) );