theorem :: FOMODEL0:34

for x2 being set
for U being non empty set
for u, u1 being Element of U holds
( ( u = u1 implies (u1,x2) -SymbolSubstIn <*u*> = <*x2*> ) & ( u <> u1 implies (u1,x2) -SymbolSubstIn <*u*> = <*u*> ) ) by Lm44;