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 set holds
( [a,b] in ExtendRel (id D) iff [a,b] in id (D * ) )

proof

let a, b be set ; :: 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:106;
A2: ( len a1 = len b1 & ( for n being Element of NAT st n in dom a1 holds
[(a1 . n),(b1 . n)] in id D ) ) by A1, Def9;

now

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, Def9;
hence a1 . n = b1 . n by RELAT_1:def 10; :: thesis: verum

end;

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

end;

assume A4: [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:106;
A5: ( a1 = b1 & len a1 = len b1 ) by A4, RELAT_1:def 10;
for n being Element of NAT st n in dom a1 holds
[(a1 . n),(b1 . n)] in id D

proof

let n be Element of 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:13;
hence [(a1 . n),(b1 . n)] in id D by A5, RELAT_1:def 10; :: thesis: verum

end;

hence [a,b] in ExtendRel (id D) by A5, Def9; :: thesis: verum

end;

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