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:58
.= FinJoin (u,(Atom (V,C))) by Th18 ; :: thesis: verum