let x2 be set ; :: thesis: 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*> ) )
let U be non empty set ; :: thesis: for u, u1 being Element of U holds
( ( u = u1 implies (u1,x2) -SymbolSubstIn <*u*> = <*x2*> ) & ( u <> u1 implies (u1,x2) -SymbolSubstIn <*u*> = <*u*> ) )
let u, u1 be Element of U; :: thesis: ( ( u = u1 implies (u1,x2) -SymbolSubstIn <*u*> = <*x2*> ) & ( u <> u1 implies (u1,x2) -SymbolSubstIn <*u*> = <*u*> ) )
set X = U;
set s = u;
set s1 = u1;
set s2 = x2;
set w = <*u*>;
set IT = (u1,x2) -SymbolSubstIn <*u*>;
set f1 = 1 .--> u1;
set f2 = 1 .--> x2;
set f = 1 .--> u;
set subst = u1 .--> x2;
set I = id U;
set w1 = <*u1*>;
set w2 = <*x2*>;
A1: ( <*u*> \+\ (1 .--> u) = {} & <*x2*> \+\ (1 .--> x2) = {} & <*u1*> \+\ (1 .--> u1) = {} ) ;
then A2: ( <*u*> = 1 .--> u & <*x2*> = 1 .--> x2 & <*u1*> = 1 .--> u1 ) by Th29;
A3: ( dom (u1 .--> x2) = {u1} & dom (1 .--> x2) = {1} & dom (1 .--> u1) = {1} & dom (1 .--> u) = {1} & rng (1 .--> u) = {u} ) by FUNCOP_1:8;
u1 in {u1} by TARSKI:def 1;
then A4: (u1 .--> x2) . u1 = x2 by FUNCOP_1:7;
A5: (u1,x2) -SymbolSubstIn <*u*> = <*u*> +* ((u1 .--> x2) * (1 .--> u)) by A1, Th29;
thus ( u = u1 implies (u1,x2) -SymbolSubstIn <*u*> = <*x2*> ) :: thesis: ( u <> u1 implies (u1,x2) -SymbolSubstIn <*u*> = <*u*> )
proof
assume A6: u = u1 ; :: thesis: (u1,x2) -SymbolSubstIn <*u*> = <*x2*>
then u in dom (u1 .--> x2) by TARSKI:def 1;
then (u1,x2) -SymbolSubstIn <*u*> = (1 .--> u) +* (1 .--> x2) by A6, A2, A4, FUNCOP_1:17
.= <*x2*> by A2, FUNCT_4:19, A3 ;
hence (u1,x2) -SymbolSubstIn <*u*> = <*x2*> ; :: thesis: verum
end;
assume u <> u1 ; :: thesis: (u1,x2) -SymbolSubstIn <*u*> = <*u*>
then (u1 .--> x2) * (1 .--> u) = {} by A3, ZFMISC_1:11, RELAT_1:44;
hence (u1,x2) -SymbolSubstIn <*u*> = <*u*> by A5; :: thesis: verum