let D be non empty set ; :: thesis: ExtendRel (id D) = id (D *)
set P = ExtendRel (id D);
set Q = id (D *);
for a, b being object holds
( [a,b] in ExtendRel (id D) iff [a,b] in id (D *) )

proof

let a, b be object ; :: thesis: ( [a,b] in ExtendRel (id D) iff [a,b] in id (D *) )
thus ( [a,b] in ExtendRel (id D) implies [a,b] in id (D *) ) :: thesis: ( [a,b] in id (D *) implies [a,b] in ExtendRel (id D) )

proof

assume A1: [a,b] in ExtendRel (id D) ; :: thesis: [a,b] in id (D *)
then reconsider a1 = a, b1 = b as Element of D * by ZFMISC_1:87;

A2: now :: thesis: for n being Nat st n in dom a1 holds
a1 . n = b1 . n

let n be Nat; :: thesis: ( n in dom a1 implies a1 . n = b1 . n )
assume n in dom a1 ; :: thesis: a1 . n = b1 . n
then [(a1 . n),(b1 . n)] in id D by A1, Def3;
hence a1 . n = b1 . n by RELAT_1:def 10; :: thesis: verum

end;

len a1 = len b1 by A1, Def3;
then a1 = b1 by A2, FINSEQ_2:9;
hence [a,b] in id (D *) by RELAT_1:def 10; :: thesis: verum

end;

assume A3: [a,b] in id (D *) ; :: thesis: [a,b] in ExtendRel (id D)
then reconsider a1 = a, b1 = b as Element of D * by ZFMISC_1:87;
A4: a1 = b1 by A3, RELAT_1:def 10;
A5: for n being Nat st n in dom a1 holds
[(a1 . n),(b1 . n)] in id D

proof

let n be Nat; :: thesis: ( n in dom a1 implies [(a1 . n),(b1 . n)] in id D )
assume n in dom a1 ; :: thesis: [(a1 . n),(b1 . n)] in id D
then a1 . n in D by FINSEQ_2:11;
hence [(a1 . n),(b1 . n)] in id D by A4, RELAT_1:def 10; :: thesis: verum

end;

len a1 = len b1 by A3, RELAT_1:def 10;
hence [a,b] in ExtendRel (id D) by A5, Def3; :: thesis: verum

end;

hence ExtendRel (id D) = id (D *) by RELAT_1:def 2; :: thesis: verum