let U be non empty set ; :: thesis: 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*> ) )
let u, u1, u2 be Element of U; :: thesis: ( ( u = u1 implies (u1 SubstWith u2) . <*u*> = <*u2*> ) & ( u <> u1 implies (u1 SubstWith u2) . <*u*> = <*u*> ) )
set e = u1 SubstWith u2;
set es = (u1,u2) -SymbolSubstIn <*u*>;
(u1,u2) -SymbolSubstIn <*u*> = (u1 SubstWith u2) . <*u*> by Def22;
hence ( ( u = u1 implies (u1 SubstWith u2) . <*u*> = <*u2*> ) & ( u <> u1 implies (u1 SubstWith u2) . <*u*> = <*u*> ) ) by Lm44; :: thesis: verum