let n be Nat; :: thesis: for ap, bp, cp, dp being FinSequence holds n -BitFTA0CarryOutput (ap,bp,cp,dp) is pair
let ap, bp, cp, dp be FinSequence; :: thesis: n -BitFTA0CarryOutput (ap,bp,cp,dp) is pair

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

suppose n = 0 ; :: thesis: n -BitFTA0CarryOutput (ap,bp,cp,dp) is pair

hence n -BitFTA0CarryOutput (ap,bp,cp,dp) is pair by LmT00CO; :: thesis: verum

end;

suppose ex m being Nat st n = m + 1 ; :: thesis: n -BitFTA0CarryOutput (ap,bp,cp,dp) is pair

then consider m being Nat such that
B1: n = m + 1 ;
n -BitFTA0CarryOutput (ap,bp,cp,dp) = GFA0CarryOutput ((ap . (m + 1)),(bp . (m + 1)),(cp . (m + 1))) by B1, LmT0COk
.= [<*[<*(ap . (m + 1)),(bp . (m + 1))*>,and2],[<*(bp . (m + 1)),(cp . (m + 1))*>,and2],[<*(cp . (m + 1)),(ap . (m + 1))*>,and2]*>,or3] ;
hence n -BitFTA0CarryOutput (ap,bp,cp,dp) is pair ; :: thesis: verum

end;

end;