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:58

.= FinJoin ((@ u),(Atom A)) by Th9 ; :: thesis: verum

let u be Element of (NormForm A); :: thesis: u = FinJoin ((@ u),(Atom A))

thus u = FinUnion ((@ u),(singleton (DISJOINT_PAIRS A))) by SETWISEO:58

.= FinJoin ((@ u),(Atom A)) by Th9 ; :: thesis: verum