let R1, R2 be Relation of F₁(),F₂(); :: thesis: ( ex F being ManySortedSet of st
( R1 = F . F₃() & F . 0 = F₄() & ( for i being Element of NAT
for R being Relation of F₁(),F₂() st R = F . i holds
F . (i + 1) = F₅(R,i) ) ) & ex F being ManySortedSet of st
( R2 = F . F₃() & F . 0 = F₄() & ( for i being Element of NAT
for R being Relation of F₁(),F₂() st R = F . i holds
F . (i + 1) = F₅(R,i) ) ) implies R1 = R2 )
given F1 being ManySortedSet of such that A1: R1 = F1 . F₃() and
A2: F1 . 0 = F₄() and
A3: for i being Element of NAT
for R being Relation of F₁(),F₂() st R = F1 . i holds
F1 . (i + 1) = F₅(R,i) ; :: thesis: ( for F being ManySortedSet of holds
( not R2 = F . F₃() or not F . 0 = F₄() or ex i being Element of NAT ex R being Relation of F₁(),F₂() st
( R = F . i & not F . (i + 1) = F₅(R,i) ) ) or R1 = R2 )
given F2 being ManySortedSet of such that A4: R2 = F2 . F₃() and
A5: F2 . 0 = F₄() and
A6: for i being Element of NAT
for R being Relation of F₁(),F₂() st R = F2 . i holds
F2 . (i + 1) = F₅(R,i) ; :: thesis: R1 = R2
defpred S₁[ Element of NAT ] means ( F1 . $1 = F2 . $1 & F1 . $1 is Relation of F₁(),F₂() );
A7: S₁[ 0 ] by A2, A5;

A8: now

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A9: S₁[i] ; :: thesis: S₁[i + 1]
then reconsider R = F1 . i as Relation of F₁(),F₂() ;
F1 . (i + 1) = F₅(R,i) by A3;
hence S₁[i + 1] by A6, A9; :: thesis: verum

end;

for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A7, A8);
hence R1 = R2 by A1, A4; :: thesis: verum