let V, C be set ; :: thesis: for B being Element of Fin (PFuncs V,C)
for a, b being set st B in SubstitutionSet V,C & a in B & b in B & a c= b holds
a = b
let B be Element of Fin (PFuncs V,C); :: thesis: for a, b being set st B in SubstitutionSet V,C & a in B & b in B & a c= b holds
a = b
let a, b be set ; :: thesis: ( B in SubstitutionSet V,C & a in B & b in B & a c= b implies a = b )
assume B in SubstitutionSet V,C ; :: thesis: ( not a in B or not b in B or not a c= b or a = b )
then A1: ex A1 being Element of Fin (PFuncs V,C) st
( A1 = B & ( for u being set st u in A1 holds
u is finite ) & ( for s, t being Element of PFuncs V,C st s in A1 & t in A1 & s c= t holds
s = t ) ) ;
assume that
A2: ( a in B & b in B ) and
A3: a c= b ; :: thesis: a = b
B c= PFuncs V,C by FINSUB_1:def 5;
then reconsider a9 = a, b9 = b as Element of PFuncs V,C by A2;
a9 = b9 by A1, A2, A3;
hence a = b ; :: thesis: verum