let ap, bm, cp, dm be FinSequence; :: thesis: 0 -BitFTA1CarryOutput (ap,bm,cp,dm) = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]
consider h being ManySortedSet of NAT such that
A1: 0 -BitFTA1CarryOutput (ap,bm,cp,dm) = h . 0 and
A2: h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] and
for k being Nat holds h . (k + 1) = BitFTA1CarryOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)),(dm . (k + 1)),(h . k)) by Def10;
thus 0 -BitFTA1CarryOutput (ap,bm,cp,dm) = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] by A1, A2; :: thesis: verum