let n be Nat; :: thesis: for ap, bm, cp, dm being FinSequence holds n -BitFTA1CarryOutput (ap,bm,cp,dm) is pair
let ap, bm, cp, dm be FinSequence; :: thesis: n -BitFTA1CarryOutput (ap,bm,cp,dm) is pair

per cases ( n = 0 or ex m being Nat st n = m + 1 ) by NAT_1:6;

suppose n = 0 ; :: thesis: n -BitFTA1CarryOutput (ap,bm,cp,dm) is pair

hence n -BitFTA1CarryOutput (ap,bm,cp,dm) is pair by LmT10CO; :: thesis: verum

end;

suppose ex m being Nat st n = m + 1 ; :: thesis: n -BitFTA1CarryOutput (ap,bm,cp,dm) is pair

then consider m being Nat such that
B1: n = m + 1 ;
n -BitFTA1CarryOutput (ap,bm,cp,dm) = GFA1CarryOutput ((ap . (m + 1)),(bm . (m + 1)),(cp . (m + 1))) by B1, LmT1COk
.= [<*[<*(ap . (m + 1)),(bm . (m + 1))*>,and2c],[<*(bm . (m + 1)),(cp . (m + 1))*>,and2a],[<*(cp . (m + 1)),(ap . (m + 1))*>,and2]*>,or3] ;
hence n -BitFTA1CarryOutput (ap,bm,cp,dm) is pair ; :: thesis: verum

end;

end;