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