let S be locally_directed OrderSortedSign; :: thesis: for o being Element of the carrier' of S
for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for x being set st x in (((OSClass R) #) * the Arity of S) . o holds
ex a being Element of Args (o,A) st x = R #_os a
let o be Element of the carrier' of S; :: thesis: for A being non-empty OSAlgebra of S
for R being OSCongruence of A
for x being set st x in (((OSClass R) #) * the Arity of S) . o holds
ex a being Element of Args (o,A) st x = R #_os a
let A be non-empty OSAlgebra of S; :: thesis: for R being OSCongruence of A
for x being set st x in (((OSClass R) #) * the Arity of S) . o holds
ex a being Element of Args (o,A) st x = R #_os a
let R be OSCongruence of A; :: thesis: for x being set st x in (((OSClass R) #) * the Arity of S) . o holds
ex a being Element of Args (o,A) st x = R #_os a
let x be set ; :: thesis: ( x in (((OSClass R) #) * the Arity of S) . o implies ex a being Element of Args (o,A) st x = R #_os a )
assume A1: x in (((OSClass R) #) * the Arity of S) . o ; :: thesis: ex a being Element of Args (o,A) st x = R #_os a
set ar = the_arity_of o;
A2: the_arity_of o = the Arity of S . o by MSUALG_1:def 1;
then (((OSClass R) #) * the Arity of S) . o = product ((OSClass R) * (the_arity_of o)) by MSAFREE:1;
then consider f being Function such that
A3: f = x and
A4: dom f = dom ((OSClass R) * (the_arity_of o)) and
A5: for y being object st y in dom ((OSClass R) * (the_arity_of o)) holds
f . y in ((OSClass R) * (the_arity_of o)) . y by A1, CARD_3:def 5;
defpred S₁[ object , object ] means ( $2 in the Sorts of A . ((the_arity_of o) /. $1) & $2 in f . $1 );
A6: dom ((OSClass R) * (the_arity_of o)) = dom (the_arity_of o) by PARTFUN1:def 2;
A7: for n being Nat st n in dom f holds
f . n in OSClass (R,((the_arity_of o) /. n))

proof

let n be Nat; :: thesis: ( n in dom f implies f . n in OSClass (R,((the_arity_of o) /. n)) )
reconsider s = (the_arity_of o) /. n as Element of S ;
assume A8: n in dom f ; :: thesis: f . n in OSClass (R,((the_arity_of o) /. n))
then (the_arity_of o) . n = (the_arity_of o) /. n by A4, A6, PARTFUN1:def 6;
then ((OSClass R) * (the_arity_of o)) . n = (OSClass R) . s by A4, A8, FUNCT_1:12
.= OSClass (R,s) by Def11 ;
hence f . n in OSClass (R,((the_arity_of o) /. n)) by A4, A5, A8; :: thesis: verum

end;

A9: for a being object st a in dom f holds
ex b being object st S₁[a,b]

proof

let a be object ; :: thesis: ( a in dom f implies ex b being object st S₁[a,b] )
reconsider s = (the_arity_of o) /. a as Element of S ;
assume A10: a in dom f ; :: thesis: ex b being object st S₁[a,b]
then reconsider n = a as Nat by A4;
f . n in OSClass (R,s) by A7, A10;
then consider x being set such that
A11: ( x in the Sorts of A . s & f . n = Class ((CompClass (R,(CComp s))),x) ) by Def10;
take x ; :: thesis: S₁[a,x]
thus S₁[a,x] by A11, Th5, EQREL_1:20; :: thesis: verum

end;

consider g being Function such that
A12: ( dom g = dom f & ( for a being object st a in dom f holds
S₁[a,g . a] ) ) from CLASSES1:sch 1(A9);
dom the Sorts of A = the carrier of S by PARTFUN1:def 2;
then rng (the_arity_of o) c= dom the Sorts of A ;
then A13: dom g = dom ( the Sorts of A * (the_arity_of o)) by A4, A6, A12, RELAT_1:27;
A14: for y being object st y in dom ( the Sorts of A * (the_arity_of o)) holds
g . y in ( the Sorts of A * (the_arity_of o)) . y

proof

let y be object ; :: thesis: ( y in dom ( the Sorts of A * (the_arity_of o)) implies g . y in ( the Sorts of A * (the_arity_of o)) . y )
assume A15: y in dom ( the Sorts of A * (the_arity_of o)) ; :: thesis: g . y in ( the Sorts of A * (the_arity_of o)) . y
then reconsider n = y as Nat ;
reconsider s = (the_arity_of o) /. n as Element of S ;
( (the_arity_of o) . n = (the_arity_of o) /. n & g . n in the Sorts of A . s ) by A4, A6, A12, A13, A15, PARTFUN1:def 6;
hence g . y in ( the Sorts of A * (the_arity_of o)) . y by A15, FUNCT_1:12; :: thesis: verum

end;

Args (o,A) = (( the Sorts of A #) * the Arity of S) . o by MSUALG_1:def 4
.= product ( the Sorts of A * (the_arity_of o)) by A2, MSAFREE:1 ;
then reconsider g = g as Element of Args (o,A) by A13, A14, CARD_3:9;
A16: for x being object st x in dom (the_arity_of o) holds
f . x = (R #_os g) . x

proof

let x be object ; :: thesis: ( x in dom (the_arity_of o) implies f . x = (R #_os g) . x )
assume A17: x in dom (the_arity_of o) ; :: thesis: f . x = (R #_os g) . x
then reconsider n = x as Nat ;
A18: ( ex z being Element of the Sorts of A . ((the_arity_of o) /. n) st
( z = g . n & (R #_os g) . n = OSClass (R,z) ) & g . n in f . n ) by A4, A6, A12, A17, Def13;
reconsider s = (the_arity_of o) /. n as Element of S ;
f . n in OSClass (R,s) by A4, A6, A7, A17;
then consider u being set such that
A19: u in the Sorts of A . s and
A20: f . n = Class ((CompClass (R,(CComp s))),u) by Def10;
u in the Sorts of A -carrier_of (CComp s) by A19, Th5;
hence f . x = (R #_os g) . x by A18, A20, EQREL_1:23; :: thesis: verum

end;

take g ; :: thesis: x = R #_os g
dom (R #_os g) = dom ((OSClass R) * (the_arity_of o)) by CARD_3:9;
hence x = R #_os g by A3, A4, A6, A16, FUNCT_1:2; :: thesis: verum