let x, y, c be set ; :: thesis: for S being non empty ManySortedSign st S = BitSubtracterWithBorrowStr x,y,c holds
( x in the carrier of S & y in the carrier of S & c in the carrier of S )
set S1 = 2GatesCircStr x,y,c,'xor' ;
set S2 = BorrowStr x,y,c;
let S be non empty ManySortedSign ; :: thesis: ( S = BitSubtracterWithBorrowStr x,y,c implies ( x in the carrier of S & y in the carrier of S & c in the carrier of S ) )
assume S = BitSubtracterWithBorrowStr x,y,c ; :: thesis: ( x in the carrier of S & y in the carrier of S & c in the carrier of S )
then ( x in the carrier of (2GatesCircStr x,y,c,'xor' ) & y in the carrier of (2GatesCircStr x,y,c,'xor' ) & c in the carrier of (2GatesCircStr x,y,c,'xor' ) & S = (2GatesCircStr x,y,c,'xor' ) +* (BorrowStr x,y,c) ) by FACIRC_1:60;
hence ( x in the carrier of S & y in the carrier of S & c in the carrier of S ) by FACIRC_1:20; :: thesis: verum