let A be set ; :: thesis: for u being Element of (NormForm A) holds u = FinJoin (@ u),(Atom A)
let u be Element of (NormForm A); :: thesis: u = FinJoin (@ u),(Atom A)
thus u = FinUnion (@ u),(singleton (DISJOINT_PAIRS A)) by SETWISEO:71
.= FinJoin (@ u),(Atom A) by Th14 ; :: thesis: verum