theorem :: FOMODEL0:35

for U being non empty set
for u, u1, u2 being Element of U holds
( ( u = u1 implies (u1 SubstWith u2) . <*u*> = <*u2*> ) & ( u <> u1 implies (u1 SubstWith u2) . <*u*> = <*u*> ) ) by Lm46;