set O = [: the carrier' of S,{ the carrier of S}:] \/ (Union ());
defpred S1[ Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union ()), Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) * ] means ( \$1 in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = \$1 holds
( len \$2 = len () & ( for x being set st x in dom \$2 holds
( ( \$2 . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = \$2 . x holds
the_result_sort_of o1 = () . x ) & ( \$2 . x in Union () implies \$2 . x in coprod ((() . x),X) ) ) ) ) ) );
consider R being Relation of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ())),(([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) *) such that
A1: for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union ())
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) * holds
( [a,b] in R iff S1[a,b] ) from take R ; :: thesis: for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union ())
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) * holds
( [a,b] in R iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len () & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = () . x ) & ( b . x in Union () implies b . x in coprod ((() . x),X) ) ) ) ) ) ) )

let a be Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union ()); :: thesis: for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) * holds
( [a,b] in R iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len () & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = () . x ) & ( b . x in Union () implies b . x in coprod ((() . x),X) ) ) ) ) ) ) )

let b be Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) * ; :: thesis: ( [a,b] in R iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len () & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = () . x ) & ( b . x in Union () implies b . x in coprod ((() . x),X) ) ) ) ) ) ) )

thus ( [a,b] in R implies ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len () & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = () . x ) & ( b . x in Union () implies b . x in coprod ((() . x),X) ) ) ) ) ) ) ) by A1; :: thesis: ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len () & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = () . x ) & ( b . x in Union () implies b . x in coprod ((() . x),X) ) ) ) ) ) implies [a,b] in R )

assume ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len () & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = () . x ) & ( b . x in Union () implies b . x in coprod ((() . x),X) ) ) ) ) ) ) ; :: thesis: [a,b] in R
hence [a,b] in R by A1; :: thesis: verum