let R be non empty RelStr ; :: thesis: for X being non empty Subset of R holds
( the mapping of (X +id ) = id X & the mapping of (X opp+id ) = id X )
let X be non empty Subset of R; :: thesis: ( the mapping of (X +id ) = id X & the mapping of (X opp+id ) = id X )
( the carrier of (X +id ) = X & the carrier of (X opp+id ) = X ) by YELLOW_9:6, YELLOW_9:7;
then A1: ( dom the mapping of (X +id ) = X & dom the mapping of (X opp+id ) = X ) by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in X implies the mapping of (X +id ) . x = x )
assume x in X ; :: thesis: the mapping of (X +id ) . x = x
then reconsider i = x as Element of (X +id ) by YELLOW_9:6;
thus the mapping of (X +id ) . x = (X +id ) . i
.= x by YELLOW_9:6 ; :: thesis: verum

end;

hence the mapping of (X +id ) = id X by A1, FUNCT_1:34; :: thesis: the mapping of (X opp+id ) = id X

now

let x be set ; :: thesis: ( x in X implies the mapping of (X opp+id ) . x = x )
assume x in X ; :: thesis: the mapping of (X opp+id ) . x = x
then reconsider i = x as Element of (X opp+id ) by YELLOW_9:7;
thus the mapping of (X opp+id ) . x = (X opp+id ) . i
.= x by YELLOW_9:7 ; :: thesis: verum

end;

hence the mapping of (X opp+id ) = id X by A1, FUNCT_1:34; :: thesis: verum