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 consider t' being Element of PFuncs V,C such that
A2: ( a = t' & t' is finite & ( for s being Element of PFuncs V,C holds
( ( s in A & s c= t' ) iff s = t' ) ) ) ;
thus a in PFuncs V,C by A2; :: thesis: verum

end;

A3: 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 { 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;
then A4: { 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 finite ;
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 M' = M as Element of Fin (PFuncs V,C) by A1, A4, FINSUB_1:def 5;
A5: for u being set st u in M' holds
u is finite

proof

let u be set ; :: thesis: ( u in M' implies u is finite )
assume u in M' ; :: thesis: u is finite
then consider t' being Element of PFuncs V,C such that
A6: ( u = t' & t' is finite & ( for s being Element of PFuncs V,C holds
( ( s in A & s c= t' ) iff s = t' ) ) ) ;
thus u is finite by A6; :: thesis: verum

end;

for s, t being Element of PFuncs V,C st s in M' & t in M' & s c= t holds
s = t

proof

let s, t be Element of PFuncs V,C; :: thesis: ( s in M' & t in M' & s c= t implies s = t )
assume A7: ( s in M' & t in M' & s c= t ) ; :: thesis: s = t
then A8: s in A by A3;
consider tt being Element of PFuncs V,C such that
A9: ( t = tt & tt is finite & ( for ss being Element of PFuncs V,C holds
( ( ss in A & ss c= tt ) iff ss = tt ) ) ) by A7;
thus s = t by A7, A8, A9; :: 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 A5;
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