theorem :: FOMODEL0:36

for x being set
for U being non empty set
for u being Element of U
for q1, q2 being b₂ -valued FinSequence holds (x SubstWith u) . (q1 ^ q2) = ((x SubstWith u) . q1) ^ ((x SubstWith u) . q2) by Lm47;