reconsider P = id the carrier of U1 as Equivalence_Relation of U1 ;
take P ; :: thesis: for n being Nat
for o1 being operation of U1 st n in dom the charact of U1 & o1 = the charact of U1 . n holds
for x, y being FinSequence of U1 st x in dom o1 & y in dom o1 & [x,y] in ExtendRel P holds
[(o1 . x),(o1 . y)] in P
let n be Nat; :: thesis: for o1 being operation of U1 st n in dom the charact of U1 & o1 = the charact of U1 . n holds
for x, y being FinSequence of U1 st x in dom o1 & y in dom o1 & [x,y] in ExtendRel P holds
[(o1 . x),(o1 . y)] in P
let o1 be operation of U1; :: thesis: ( n in dom the charact of U1 & o1 = the charact of U1 . n implies for x, y being FinSequence of U1 st x in dom o1 & y in dom o1 & [x,y] in ExtendRel P holds
[(o1 . x),(o1 . y)] in P )
assume that
n in dom the charact of U1 and
o1 = the charact of U1 . n ; :: thesis: for x, y being FinSequence of U1 st x in dom o1 & y in dom o1 & [x,y] in ExtendRel P holds
[(o1 . x),(o1 . y)] in P
let x, y be FinSequence of U1; :: thesis: ( x in dom o1 & y in dom o1 & [x,y] in ExtendRel P implies [(o1 . x),(o1 . y)] in P )
assume that
A1: x in dom o1 and
y in dom o1 and
A2: [x,y] in ExtendRel P ; :: thesis: [(o1 . x),(o1 . y)] in P
[x,y] in id ( the carrier of U1 *) by A2, FINSEQ_3:121;
then A3: x = y by RELAT_1:def 10;
o1 . x in rng o1 by A1, FUNCT_1:def 3;
hence [(o1 . x),(o1 . y)] in P by A3, RELAT_1:def 10; :: thesis: verum