let A be QC-alphabet ; :: thesis: for k being Nat
for f being Substitution of A
for x being bound_QC-variable of A
for a being free_QC-variable of A
for l, ll being FinSequence of QC-variables A 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 k be Nat; :: thesis: for f being Substitution of A
for x being bound_QC-variable of A
for a being free_QC-variable of A
for l, ll being FinSequence of QC-variables A 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 of A; :: thesis: for x being bound_QC-variable of A
for a being free_QC-variable of A
for l, ll being FinSequence of QC-variables A 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 of A; :: thesis: for a being free_QC-variable of A
for l, ll being FinSequence of QC-variables A 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 of A; :: thesis: for l, ll being FinSequence of QC-variables A 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 l, ll be FinSequence of QC-variables A; :: 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 ) ) )
set f9 = a .--> x;
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 ) )
thus ( l . k = a implies ll . k = x ) :: thesis: ( l . k <> a implies ll . k = l . k )
proof
A2: (a .--> x) . a = x by FUNCOP_1:72;
assume A3: l . k = a ; :: thesis: ll . k = x
then l . k in {a} by TARSKI:def 1;
then l . k in dom (a .--> x) ;
hence ll . k = x by A1, A3, A2, Def1; :: 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) ;
hence ll . k = l . k by A1, Def1; :: thesis: verum