let o1, o2 be Element of InnerVertices (n -BitSubtracterStr (x,y)); :: thesis: ( ex h being ManySortedSet of NAT st
( o1 = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat holds h . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) ) & ex h being ManySortedSet of NAT st
( o2 = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat holds h . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) ) implies o1 = o2 )
given h1 being ManySortedSet of NAT such that A1: o1 = h1 . n and
A2: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] and
A3: for n being Nat holds h1 . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),(h1 . n)) ; :: thesis: ( for h being ManySortedSet of NAT holds
( not o2 = h . n or not h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] or ex n being Nat st not h . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) or o1 = o2 )
given h2 being ManySortedSet of NAT such that A4: o2 = h2 . n and
A5: h2 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] and
A6: for n being Nat holds h2 . (n + 1) = BorrowOutput ((x . (n + 1)),(y . (n + 1)),(h2 . n)) ; :: thesis: o1 = o2
deffunc H₁( Nat, set ) -> Element of InnerVertices (BorrowStr ((x . ($1 + 1)),(y . ($1 + 1)),$2)) = BorrowOutput ((x . ($1 + 1)),(y . ($1 + 1)),$2);
A7: dom h1 = NAT by PARTFUN1:def 2;
A8: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] by A2;
A9: for n being Nat holds h1 . (n + 1) = H₁(n,h1 . n) by A3;
A10: dom h2 = NAT by PARTFUN1:def 2;
A11: h2 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] by A5;
A12: for n being Nat holds h2 . (n + 1) = H₁(n,h2 . n) by A6;
h1 = h2 from NAT_1:sch 15(A7, A8, A9, A10, A11, A12);
hence o1 = o2 by A1, A4; :: thesis: verum