let A be QC-alphabet ; 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; 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; 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; 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; 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; ( 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 )
; ( ( l . k = a implies ll . k = x ) & ( l . k <> a implies ll . k = l . k ) )
thus
( l . k = a implies ll . k = x )
( l . k <> a implies ll . k = l . k )
assume
l . k <> a
; 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; verum