A1: ex h being ManySortedSet of NAT st
( 0 -BitBorrowOutput (x,y) = h . 0 & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat holds h . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) ) by Def3;
defpred S₁[ Element of NAT ] means n -BitBorrowOutput (x,y) is pair ;
A2: S₁[ 0 ] by A1;
A3: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
(n + 1) -BitBorrowOutput (x,y) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),(n -BitBorrowOutput (x,y))) by Th7
.= [<*[<*(x . (n + 1)),(y . (n + 1))*>,and2a],[<*(y . (n + 1)),(n -BitBorrowOutput (x,y))*>,and2],[<*(x . (n + 1)),(n -BitBorrowOutput (x,y))*>,and2a]*>,or3] ;
hence ( S₁[n] implies S₁[n + 1] ) ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A3);
hence n -BitBorrowOutput (x,y) is pair ; :: thesis: verum