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