deffunc H₁( object ) -> Element of bool [:(A . $1),(A . $1):] = id (A . $1);
A1: for i being set st i in I holds
H₁(i) is Relation of (A . i),(A . i) ;
( ex R being ManySortedRelation of A st
for i being object st i in I holds
R . i = H₁(i) & ( for R1, R2 being ManySortedRelation of A st ( for i being object st i in I holds
R1 . i = H₁(i) ) & ( for i being object st i in I holds
R2 . i = H₁(i) ) holds
R1 = R2 ) ) from MSUALG_6:sch 3(A1);
hence ( ex b₁ being ManySortedRelation of A st
for i being object st i in I holds
b₁ . i = id (A . i) & ( for b₁, b₂ being ManySortedRelation of A st ( for i being object st i in I holds
b₁ . i = id (A . i) ) & ( for i being object st i in I holds
b₂ . i = id (A . i) ) holds
b₁ = b₂ ) ) ; :: thesis: verum