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 set ; :: 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

let x be set ; :: 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 by TARSKI:def 3;
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