let V be set ; :: thesis: for C being finite set
for u being Element of SubstitutionSet V,C holds u = FinJoin u,(Atom V,C)
let C be finite set ; :: thesis: for u being Element of SubstitutionSet V,C holds u = FinJoin u,(Atom V,C)
let u be Element of SubstitutionSet V,C; :: thesis: u = FinJoin u,(Atom V,C)
thus u = FinUnion u,(singleton (PFuncs V,C)) by SETWISEO:71
.= FinJoin u,(Atom V,C) by Th23 ; :: thesis: verum