let k be Element of NAT ; :: thesis: for x being bound_QC-variable
for a being free_QC-variable
for ll, l being FinSequence of QC-variables
for f being Substitution st f = a .--> x & ll = Subst l,f & 1 <= k & k <= len l holds
( ( l . k = a implies ll . k = x ) & ( l . k <> a implies ll . k = l . k ) )
let x be bound_QC-variable; :: thesis: for a being free_QC-variable
for ll, l being FinSequence of QC-variables
for f being Substitution st f = a .--> x & ll = Subst l,f & 1 <= k & k <= len l holds
( ( l . k = a implies ll . k = x ) & ( l . k <> a implies ll . k = l . k ) )
let a be free_QC-variable; :: thesis: for ll, l being FinSequence of QC-variables
for f being Substitution st f = a .--> x & ll = Subst l,f & 1 <= k & k <= len l holds
( ( l . k = a implies ll . k = x ) & ( l . k <> a implies ll . k = l . k ) )
let ll, l be FinSequence of QC-variables ; :: thesis: for f being Substitution st f = a .--> x & ll = Subst l,f & 1 <= k & k <= len l holds
( ( l . k = a implies ll . k = x ) & ( l . k <> a implies ll . k = l . k ) )
let f be Substitution; :: thesis: ( f = a .--> x & ll = Subst l,f & 1 <= k & k <= len l implies ( ( l . k = a implies ll . k = x ) & ( l . k <> a implies ll . k = l . k ) ) )
assume A1: ( f = a .--> x & ll = Subst l,f & 1 <= k & k <= len l ) ; :: thesis: ( ( l . k = a implies ll . k = x ) & ( l . k <> a implies ll . k = l . k ) )
set f' = a .--> x;
thus ( l . k = a implies ll . k = x ) :: thesis: ( l . k <> a implies ll . k = l . k )

proof

assume A2: l . k = a ; :: thesis: ll . k = x
then l . k in {a} by TARSKI:def 1;
then ( l . k in dom (a .--> x) & (a .--> x) . a = x ) by FUNCOP_1:19, FUNCOP_1:87;
hence ll . k = x by A1, A2, Def3; :: thesis: verum

end;

assume l . k <> a ; :: thesis: ll . k = l . k
then not l . k in {a} by TARSKI:def 1;
then not l . k in dom (a .--> x) by FUNCOP_1:19;
hence ll . k = l . k by A1, Def3; :: thesis: verum