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