set M = { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) } ;
A1: { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) } c= PFuncs (V,C)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) } or a in PFuncs (V,C) )
assume a in { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) } ; :: thesis: a in PFuncs (V,C)
then ex t9 being Element of PFuncs (V,C) st
( a = t9 & t9 is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t9 ) iff s = t9 ) ) ) ;
hence a in PFuncs (V,C) ; :: thesis: verum

end;

A2: now :: thesis: for x being object st x in { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) } holds
x in A

let x be object ; :: thesis: ( x in { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) } implies x in A )
assume x in { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) } ; :: thesis: x in A
then ex t being Element of PFuncs (V,C) st
( x = t & t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) ;
hence x in A ; :: thesis: verum

end;

then A3: { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) } c= A ;
reconsider M = { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) } as set ;
reconsider M9 = M as Element of Fin (PFuncs (V,C)) by A1, A3, FINSUB_1:def 5;
A4: for u being set st u in M9 holds
u is finite

proof

let u be set ; :: thesis: ( u in M9 implies u is finite )
assume u in M9 ; :: thesis: u is finite
then ex t9 being Element of PFuncs (V,C) st
( u = t9 & t9 is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t9 ) iff s = t9 ) ) ) ;
hence u is finite ; :: thesis: verum

end;

for s, t being Element of PFuncs (V,C) st s in M9 & t in M9 & s c= t holds
s = t

proof

let s, t be Element of PFuncs (V,C); :: thesis: ( s in M9 & t in M9 & s c= t implies s = t )
assume that
A5: ( s in M9 & t in M9 ) and
A6: s c= t ; :: thesis: s = t
( s in A & ex tt being Element of PFuncs (V,C) st
( t = tt & tt is finite & ( for ss being Element of PFuncs (V,C) holds
( ( ss in A & ss c= tt ) iff ss = tt ) ) ) ) by A2, A5;
hence s = t by A6; :: thesis: verum

end;

then M in { A1 where A1 is Element of Fin (PFuncs (V,C)) : ( ( 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 ) ) } by A4;
hence { t where t is Element of PFuncs (V,C) : ( t is finite & ( for s being Element of PFuncs (V,C) holds
( ( s in A & s c= t ) iff s = t ) ) ) } is Element of SubstitutionSet (V,C) ; :: thesis: verum