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 ) ) ;
A2: B c= PFuncs V,C by FINSUB_1:def 5;
assume A3: ( a in B & b in B & a c= b ) ; :: thesis: a = b
then reconsider a' = a, b' = b as Element of PFuncs V,C by A2;
a' = b' by A1, A3;
hence a = b ; :: thesis: verum