defpred S1[ object , object ] means ex k1, k2 being Element of commaMorphs (F,G) st
( $1 = [k1,k2] & $2 = k1 * k2 );
set X = { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } ;
A1: for x being object st x in { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } implies ex y being object st S1[x,y] )
assume x in { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } ; :: thesis: ex y being object st S1[x,y]
then consider k1, k2 being Element of commaMorphs (F,G) such that
A2: x = [k1,k2] and
k1 `11 = k2 `12 ;
reconsider y = k1 * k2 as set ;
take y ; :: thesis: S1[x,y]
take k1 ; :: thesis: ex k2 being Element of commaMorphs (F,G) st
( x = [k1,k2] & y = k1 * k2 )
take k2 ; :: thesis: ( x = [k1,k2] & y = k1 * k2 )
thus ( x = [k1,k2] & y = k1 * k2 ) by A2; :: thesis: verum
end;
consider f being Function such that
A3: ( dom f = { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } & ( for x being object st x in { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } holds
S1[x,f . x] ) ) from CLASSES1:sch 1(A1);
 A4: rng f c= commaMorphs (F,G)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in commaMorphs (F,G) )
assume x in rng f ; :: thesis: x in commaMorphs (F,G)
then consider y being object such that
A5: y in dom f and
A6: x = f . y by FUNCT_1:def 3;
ex k1, k2 being Element of commaMorphs (F,G) st
( y = [k1,k2] & f . y = k1 * k2 ) by A3, A5;
hence x in commaMorphs (F,G) by A6; :: thesis: verum
end;
dom f c= [:(commaMorphs (F,G)),(commaMorphs (F,G)):]
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in [:(commaMorphs (F,G)),(commaMorphs (F,G)):] )
assume x in dom f ; :: thesis: x in [:(commaMorphs (F,G)),(commaMorphs (F,G)):]
then ex k1, k2 being Element of commaMorphs (F,G) st
( x = [k1,k2] & k1 `11 = k2 `12 ) by A3;
hence x in [:(commaMorphs (F,G)),(commaMorphs (F,G)):] ; :: thesis: verum
end;
then reconsider f = f as PartFunc of [:(commaMorphs (F,G)),(commaMorphs (F,G)):],(commaMorphs (F,G)) by A4, RELSET_1:4;
take f ; :: thesis: ( dom f = { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } & ( for k, k9 being Element of commaMorphs (F,G) st [k,k9] in dom f holds
f . [k,k9] = k * k9 ) )
thus dom f = { [k1,k2] where k1, k2 is Element of commaMorphs (F,G) : k1 `11 = k2 `12 } by A3; :: thesis: for k, k9 being Element of commaMorphs (F,G) st [k,k9] in dom f holds
f . [k,k9] = k * k9
let k1, k2 be Element of commaMorphs (F,G); :: thesis: ( [k1,k2] in dom f implies f . [k1,k2] = k1 * k2 )
assume [k1,k2] in dom f ; :: thesis: f . [k1,k2] = k1 * k2
then consider k, k9 being Element of commaMorphs (F,G) such that
A7: [k1,k2] = [k,k9] and
A8: f . [k1,k2] = k * k9 by A3;
k1 = k by A7, XTUPLE_0:1;
hence f . [k1,k2] = k1 * k2 by A7, A8, XTUPLE_0:1; :: thesis: verum