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 )

A1: now :: thesis: for x being object st x in X holds
the mapping of (X +id) . x = x

let x be object ; :: 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;

the carrier of (X +id) = X by YELLOW_9:6;
then dom the mapping of (X +id) = X by FUNCT_2:def 1;
hence the mapping of (X +id) = id X by A1, FUNCT_1:17; :: thesis: the mapping of (X opp+id) = id X

A2: now :: thesis: for x being object st x in X holds
the mapping of (X opp+id) . x = x

let x be object ; :: 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;

the carrier of (X opp+id) = X by YELLOW_9:7;
then dom the mapping of (X opp+id) = X by FUNCT_2:def 1;
hence the mapping of (X opp+id) = id X by A2, FUNCT_1:17; :: thesis: verum