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